diff options
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 |