diff -r f54b061c2c22 -r 17090e27aae9 src/HOL/Tools/Transfer/transfer.ML
--- a/src/HOL/Tools/Transfer/transfer.ML	Wed Aug 25 22:17:38 2021 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML	Thu Aug 26 14:45:19 2021 +0200
@@ -575,7 +575,7 @@
       ((Name.clean_index (prep a, idx), \<^typ>\<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>), Thm.cterm_of ctxt' t)
   in
     thm
-    |> Thm.generalize (tfrees, rnames @ frees) idx
+    |> Thm.generalize (Symtab.make_set tfrees, Symtab.make_set (rnames @ frees)) idx
     |> Thm.instantiate (map tinst binsts, map inst binsts)
   end
 
@@ -596,7 +596,7 @@
       ((Name.clean_index (prep a, idx), \<^typ>\<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>), Thm.cterm_of ctxt' t)
   in
     thm
-    |> Thm.generalize (tfrees, rnames @ frees) idx
+    |> Thm.generalize (Symtab.make_set tfrees, Symtab.make_set (rnames @ frees)) idx
     |> Thm.instantiate (map tinst binsts, map inst binsts)
   end
 
@@ -718,7 +718,8 @@
             raise TERM ("Transfer failed to convert goal to an object-logic formula", ts))
     |> Raw_Simplifier.rewrite_rule ctxt' post_simps
     |> Simplifier.norm_hhf ctxt'
-    |> Drule.generalize (map (fst o dest_TFree o Thm.typ_of o snd) instT, [])
+    |> Drule.generalize
+        (Symtab.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Symtab.empty)
     |> Drule.zero_var_indexes
   end
 (*
@@ -753,7 +754,8 @@
             raise TERM ("Transfer failed to convert goal to an object-logic formula", ts))
     |> Raw_Simplifier.rewrite_rule ctxt' post_simps
     |> Simplifier.norm_hhf ctxt'
-    |> Drule.generalize (map (fst o dest_TFree o Thm.typ_of o snd) instT, [])
+    |> Drule.generalize
+        (Symtab.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Symtab.empty)
     |> Drule.zero_var_indexes
   end