diff -r 7829d6435c60 -r c2ee8d993d6a src/Pure/goal.ML
--- a/src/Pure/goal.ML	Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Pure/goal.ML	Fri Sep 10 14:59:19 2021 +0200
@@ -58,7 +58,7 @@
   -------- (init)
   C \<Longrightarrow> #C
 *)
-fun init C = Thm.instantiate ([], [((("A", 0), propT), C)]) Drule.protectI;
+fun init C = Thm.instantiate (TVars.empty, Vars.make [((("A", 0), propT), C)]) Drule.protectI;
 
 (*
   A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> C
@@ -122,8 +122,8 @@
     val tfrees = TFrees.build (fold TFrees.add_tfrees (prop :: As));
     val Ts = Names.build (TFrees.fold (Names.add_set o #1 o #1) tfrees);
     val instT =
-      build (tfrees |> TFrees.fold (fn ((a, S), _) =>
-        cons (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S)))));
+      TVars.build (tfrees |> TFrees.fold (fn ((a, S), _) =>
+        TVars.add (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S)))));
 
     val global_prop =
       Logic.list_implies (As, prop)
@@ -142,7 +142,7 @@
     val local_result =
       Thm.future global_result global_prop
       |> Thm.close_derivation \<^here>
-      |> Thm.instantiate (instT, [])
+      |> Thm.instantiate (instT, Vars.empty)
       |> Drule.forall_elim_list xs
       |> fold (Thm.elim_implies o Thm.assume) assms
       |> Thm.solve_constraints;