--- a/src/HOL/Library/rewrite.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Library/rewrite.ML Fri Sep 10 14:59:19 2021 +0200
@@ -272,7 +272,7 @@
((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