diff options
| author | stuebinm | 2022-06-29 01:14:51 +0200 |
|---|---|---|
| committer | stuebinm | 2022-06-29 01:23:31 +0200 |
| commit | cb4139dc35527bd8c8f9b70753c3d1f552c5f19d (patch) | |
| tree | 8e5709039197ad6d72d8b38235a982bf687e2608 /mltt/core/comp.ML | |
| parent | 5655750e12d3459c1237588f8dec3fc883a966b7 (diff) | |
make mltt work with isabelle 2021-1
notably, this modifies the proof method `this`: the previous version
of it no longer works with cconv.ML (borrowed from HOL), so now it's
just a call to the simplifier, which does work.
Unfortunately the new `this` can otherwise do less than the old one
(it does not instantiate schematic variables), so the old one is now
available as `infer` instead.
Diffstat (limited to 'mltt/core/comp.ML')
| -rw-r--r-- | mltt/core/comp.ML | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mltt/core/comp.ML b/mltt/core/comp.ML index 2e50753..8725ba3 100644 --- a/mltt/core/comp.ML +++ b/mltt/core/comp.ML @@ -279,7 +279,7 @@ fun comps_pconv to thms ctxt (tyenv, env_ts) = ((s, norm_type env T), Thm.cterm_of ctxt (Envir.norm_term env (Var x)))) val tyinsts = Term.add_tvars prop [] |> map (fn x => (x, Thm.ctyp_of ctxt (norm_type env (TVar x)))) - in Drule.instantiate_normalize (tyinsts, insts) thm end + in Drule.instantiate_normalize (TVars.make tyinsts, Vars.make insts) thm end fun unify_with_rhs context to env thm = let |