--- a/src/Pure/Isar/generic_target.ML Thu Sep 09 23:05:33 2021 +0200
+++ b/src/Pure/Isar/generic_target.ML Thu Sep 09 23:07:02 2021 +0200
@@ -306,8 +306,12 @@
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