more scalable operations;

--- 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

--- a/src/Pure/Isar/subgoal.ML	Thu Sep 09 23:05:33 2021 +0200
+++ b/src/Pure/Isar/subgoal.ML	Thu Sep 09 23:07:02 2021 +0200
@@ -89,7 +89,7 @@
 
     val prop = Thm.full_prop_of th';
     val concl_vars = Vars.build (Vars.add_vars (Logic.strip_imp_concl prop));
-    val vars = build_rev (Term.add_vars prop);
+    val vars = Vars.build (Vars.add_vars prop) |> Vars.list_set;
     val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
 
     fun var_inst v y =

--- a/src/Pure/Tools/rule_insts.ML	Thu Sep 09 23:05:33 2021 +0200
+++ b/src/Pure/Tools/rule_insts.ML	Thu Sep 09 23:07:02 2021 +0200
@@ -173,8 +173,8 @@
       | zip_vars ((x, _) :: xs) (SOME t :: rest) = ((x, Position.none), t) :: zip_vars xs rest
       | zip_vars [] _ = error "More instantiations than variables in theorem";
     val insts =
-      zip_vars (build_rev (Term.add_vars (Thm.full_prop_of thm))) args @
-      zip_vars (build_rev (Term.add_vars (Thm.concl_of thm))) concl_args;
+      zip_vars (Vars.build (Vars.add_vars (Thm.full_prop_of thm)) |> Vars.list_set) args @
+      zip_vars (Vars.build (Vars.add_vars (Thm.concl_of thm)) |> Vars.list_set) concl_args;
   in where_rule ctxt insts fixes thm end;
 
 fun read_instantiate ctxt insts xs =

--- a/src/Pure/logic.ML	Thu Sep 09 23:05:33 2021 +0200
+++ b/src/Pure/logic.ML	Thu Sep 09 23:07:02 2021 +0200
@@ -425,7 +425,8 @@
 fun occs (t, u) = exists_subterm (fn s => t aconv s) u;
 
 (*Close up a formula over all free variables by quantification*)
-fun close_form A = fold (all o Free) (Term.add_frees A []) A;
+fun close_form A =
+  fold_rev (all o Free) (Frees.build (Frees.add_frees A) |> Frees.list_set) A;
 
 
 

--- a/src/Pure/type_infer.ML	Thu Sep 09 23:05:33 2021 +0200
+++ b/src/Pure/type_infer.ML	Thu Sep 09 23:07:02 2021 +0200
@@ -116,8 +116,9 @@
           val used' = Name.declare a used;
         in (TVars.add ((xi, S), TFree (a, improve_sort S)) inst, used') end
       else (inst, used);
+    val params = TVars.build (fold TVars.add_tvars ts) |> TVars.list_set;
     val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt);
-    val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) (TVars.empty, used);
+    val (inst, _) = fold subst_param params (TVars.empty, used);
   in (map o map_types) (Term_Subst.instantiateT inst) ts end;
 
 end;

--- a/src/Pure/variable.ML	Thu Sep 09 23:05:33 2021 +0200
+++ b/src/Pure/variable.ML	Thu Sep 09 23:07:02 2021 +0200
@@ -590,7 +590,7 @@
 
 fun importT_inst ts ctxt =
   let
-    val tvars = build_rev (fold Term.add_tvars ts);
+    val tvars = TVars.build (fold TVars.add_tvars ts) |> TVars.list_set;
     val (tfrees, ctxt') = invent_types (map #2 tvars) ctxt;
     val instT = TVars.build (fold2 (fn a => fn b => TVars.add (a, TFree b)) tvars tfrees);
   in (instT, ctxt') end;
@@ -599,7 +599,9 @@
   let
     val ren = Name.clean #> (if is_open then I else Name.internal);
     val (instT, ctxt') = importT_inst ts ctxt;
-    val vars = map (apsnd (Term_Subst.instantiateT instT)) (build_rev (fold Term.add_vars ts));
+    val vars =
+      Vars.build (fold Vars.add_vars ts) |> Vars.list_set
+      |> map (apsnd (Term_Subst.instantiateT instT));
     val (ys, ctxt'') = variant_fixes (map (ren o #1 o #1) vars) ctxt';
     val inst = Vars.build (fold2 (fn (x, T) => fn y => Vars.add ((x, T), Free (y, T))) vars ys);
   in ((instT, inst), ctxt'') end;