diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/reification.ML
--- a/src/HOL/Tools/reification.ML	Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/reification.ML	Fri Sep 10 14:59:19 2021 +0200
@@ -176,7 +176,7 @@
               (Vartab.dest tyenv);
         in
           ((map (Thm.cterm_of ctxt) fts ~~ replicate (length fts) ctxt,
-             apfst (FWD (Drule.instantiate_normalize (ctyenv, its) cong))), bds)
+             apfst (FWD (Drule.instantiate_normalize (TVars.make ctyenv, Vars.make its) cong))), bds)
         end handle Pattern.MATCH => decomp_reify da congs (ct, ctxt) bds))
   end;
 
@@ -229,10 +229,11 @@
               (map (fn n => (n, 0)) xns) tml);
         val substt =
           let
-            val ih = Drule.cterm_rule (Thm.instantiate (subst_ty, []));
+            val ih = Drule.cterm_rule (Thm.instantiate (TVars.make subst_ty, Vars.empty));
           in map (apply2 ih) (subst_ns @ subst_vs @ cts) end;
         val th =
-          (Drule.instantiate_normalize (subst_ty, map (apfst (dest_Var o Thm.term_of)) substt) eq)
+          (Drule.instantiate_normalize
+            (TVars.make subst_ty, Vars.make (map (apfst (dest_Var o Thm.term_of)) substt)) eq)
             RS sym;
       in (hd (Variable.export ctxt'' ctxt [th]), bds) end)
       handle Pattern.MATCH => tryeqs eqs (ct, ctxt) bds);
@@ -270,7 +271,7 @@
         val (_, _ :: vs) = eq |> Thm.prop_of |> HOLogic.dest_Trueprop
           |> HOLogic.dest_eq |> fst |> strip_comb;
         val subst = map_filter (fn Var v => SOME (v, subst (#2 v)) | _ => NONE) vs;
-      in Thm.instantiate ([], subst) eq end;
+      in Thm.instantiate (TVars.empty, Vars.make subst) eq end;
     val (ps, congs) = map_split (mk_congeq ctxt' fs o prep_eq) eqs;
     val bds = AList.make (K ([], [])) tys;
   in (ps ~~ Variable.export ctxt' ctxt congs, bds) end
@@ -288,7 +289,7 @@
     val vs = map (fn Var (v as (_, T)) =>
       (v, the (AList.lookup Type.could_unify bds' T) |> snd |> HOLogic.mk_list (dest_listT T))) vars;
     val th' =
-      Drule.instantiate_normalize ([], map (apsnd (Thm.cterm_of ctxt)) vs) th;
+      Drule.instantiate_normalize (TVars.empty, Vars.make (map (apsnd (Thm.cterm_of ctxt)) vs)) th;
     val th'' = Thm.symmetric (dereify ctxt [] (Thm.lhs_of th'));
   in Thm.transitive th'' th' end;