src/Pure/Isar/generic_target.ML

     val th = Goal.norm_result ctxt raw_th;
     val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th;
     val asms' = map (rewrite_rule ctxt (Drule.norm_hhf_eqs @ defs)) asms;
 
     (*export fixes*)
-    val tfrees = map TFree (Thm.fold_terms {hyps = true} Term.add_tfrees th' []);
-    val frees = map Free (Thm.fold_terms {hyps = true} Term.add_frees th' []);
+    val tfrees =
+      TFrees.build (Thm.fold_terms {hyps = true} TFrees.add_tfrees th')
+      |> TFrees.list_set_rev |> map TFree;
+    val frees =
+      Frees.build (Thm.fold_terms {hyps = true} Frees.add_frees th')
+      |> Frees.list_set_rev |> map Free;
     val (th'' :: vs) =
       (th' :: map (Drule.mk_term o Thm.cterm_of ctxt) (map Logic.mk_type tfrees @ frees))
       |> Variable.export ctxt thy_ctxt
       |> Drule.zero_var_indexes_list;