more scalable operations;

--- a/src/Pure/Isar/generic_target.ML	Sat Sep 04 14:46:32 2021 +0200
+++ b/src/Pure/Isar/generic_target.ML	Sat Sep 04 18:21:58 2021 +0200
@@ -95,8 +95,11 @@
     val u = fold_rev lambda term_params rhs';
     val global_rhs = singleton (Variable.polymorphic thy_ctxt) u;
 
+    val type_tfrees = Term_Subst.add_tfreesT (Term.fastype_of u) Term_Subst.TFrees.empty;
     val extra_tfrees =
-      subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []);
+      (u, []) |-> (Term.fold_types o Term.fold_atyps)
+        (fn TFree v => not (Term_Subst.TFrees.defined type_tfrees v) ? insert (op =) v | _ => I)
+      |> rev;
     val type_params = map (Logic.mk_type o TFree) extra_tfrees;
   in (global_rhs, (extra_tfrees, (type_params, term_params))) end;
 
@@ -259,8 +262,14 @@
 
     val xs = Variable.add_fixed lthy rhs' [];
     val T = Term.fastype_of rhs;
-    val tfreesT = Term.add_tfreesT T (fold (Term.add_tfreesT o #2) xs []);
-    val extra_tfrees = rev (subtract (op =) tfreesT (Term.add_tfrees rhs []));
+    val type_tfrees =
+      Term_Subst.TFrees.empty
+      |> Term_Subst.add_tfreesT T
+      |> fold (Term_Subst.add_tfreesT o #2) xs;
+    val extra_tfrees =
+      (rhs, []) |-> (Term.fold_types o Term.fold_atyps)
+        (fn TFree v => not (Term_Subst.TFrees.defined type_tfrees v) ? insert (op =) v | _ => I)
+      |> rev;
     val mx' = check_mixfix lthy (b, extra_tfrees) mx;
 
     val type_params = map (Logic.mk_type o TFree) extra_tfrees;

--- a/src/Pure/Isar/obtain.ML	Sat Sep 04 14:46:32 2021 +0200
+++ b/src/Pure/Isar/obtain.ML	Sat Sep 04 18:21:58 2021 +0200
@@ -103,8 +103,11 @@
 
 fun mk_all_internal ctxt (y, z) t =
   let
+    val frees =
+      (t, Term_Subst.Frees.empty)
+      |-> Term.fold_aterms (fn Free v => Term_Subst.Frees.add (v, ()) | _ => I);
     val T =
-      (case AList.lookup (op =) (Term.add_frees t []) z of
+      (case Term_Subst.Frees.get_first (fn ((x, T), ()) => if x = z then SOME T else NONE) frees of
         SOME T => T
       | NONE => the_default dummyT (Variable.default_type ctxt z));
   in Logic.all_const T $ Term.lambda_name (y, Free (z, T)) t end;
@@ -325,11 +328,15 @@
     val terms = map (Drule.mk_term o Thm.cterm_of ctxt o Free) (xs @ ys');
 
     val instT =
-      fold (Term.add_tvarsT o #2) params []
-      |> map (fn v => (v, Thm.ctyp_of ctxt (norm_type (TVar v))));
+      (params, Term_Subst.TVars.empty) |-> fold (#2 #> Term.fold_atyps (fn T => fn instT =>
+        (case T of
+          TVar v =>
+            if Term_Subst.TVars.defined instT v then instT
+            else Term_Subst.TVars.update (v, Thm.ctyp_of ctxt (norm_type T)) instT
+        | _ => instT)));
     val closed_rule = rule
       |> Thm.forall_intr (Thm.cterm_of ctxt (Free thesis_var))
-      |> Thm.instantiate (instT, []);
+      |> Thm.instantiate (Term_Subst.TVars.dest instT, []);
 
     val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt;
     val vars' =

--- a/src/Pure/Isar/specification.ML	Sat Sep 04 14:46:32 2021 +0200
+++ b/src/Pure/Isar/specification.ML	Sat Sep 04 18:21:58 2021 +0200
@@ -281,7 +281,7 @@
 
     val _ =
       Proof_Display.print_consts int (Position.thread_data ()) lthy5
-        (member (op =) (Term.add_frees lhs' [])) [(x, T)];
+        (Term_Subst.Frees.defined (Term_Subst.add_frees lhs' Term_Subst.Frees.empty)) [(x, T)];
   in ((lhs, (def_name, th')), lthy5) end;
 
 val definition' = gen_def check_spec_open (K I);

--- a/src/Pure/Isar/subgoal.ML	Sat Sep 04 14:46:32 2021 +0200
+++ b/src/Pure/Isar/subgoal.ML	Sat Sep 04 18:21:58 2021 +0200
@@ -88,7 +88,7 @@
     val ts = map Thm.term_of params;
 
     val prop = Thm.full_prop_of th';
-    val concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [];
+    val concl_vars = Term_Subst.add_vars (Logic.strip_imp_concl prop) Term_Subst.Vars.empty;
     val vars = rev (Term.add_vars prop []);
     val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
 
@@ -96,7 +96,7 @@
       let
         val ((x, i), T) = v;
         val (U, args) =
-          if member (op =) concl_vars v then (T, [])
+          if Term_Subst.Vars.defined concl_vars v then (T, [])
           else (Ts ---> T, ts);
         val u = Free (y, U);
         in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;

--- a/src/Pure/drule.ML	Sat Sep 04 14:46:32 2021 +0200
+++ b/src/Pure/drule.ML	Sat Sep 04 18:21:58 2021 +0200
@@ -185,11 +185,18 @@
       |> map (fn (x, T) => Var ((x, maxidx + 1), Logic.incr_tvar (maxidx + 1) T));
     val Ts = map Term.fastype_of ps;
     val inst =
-      Thm.fold_terms Term.add_vars th []
-      |> map (fn (xi, T) => ((xi, T), Thm.cterm_of ctxt (Term.list_comb (Var (xi, Ts ---> T), ps))));
+      (th, Term_Subst.Vars.empty) |-> (Thm.fold_terms o Term.fold_aterms)
+        (fn t => fn inst =>
+          (case t of
+            Var (xi, T) =>
+              if Term_Subst.Vars.defined inst (xi, T) then inst
+              else
+                let val ct = Thm.cterm_of ctxt (Term.list_comb (Var (xi, Ts ---> T), ps))
+                in Term_Subst.Vars.update ((xi, T), ct) inst end
+          | _ => inst));
   in
     th
-    |> Thm.instantiate ([], inst)
+    |> Thm.instantiate ([], Term_Subst.Vars.dest inst)
     |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) ps
   end;
 

--- a/src/Pure/more_thm.ML	Sat Sep 04 14:46:32 2021 +0200
+++ b/src/Pure/more_thm.ML	Sat Sep 04 18:21:58 2021 +0200
@@ -449,11 +449,13 @@
 fun forall_intr_frees th =
   let
     val fixed =
-      fold Term.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th) @ Thm.hyps_of th) [];
+      Term_Subst.Frees.empty
+      |> fold Term_Subst.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th))
+      |> fold Term_Subst.add_frees (Thm.hyps_of th);
     val frees =
       Thm.fold_atomic_cterms (fn a =>
         (case Thm.term_of a of
-          Free v => not (member (op =) fixed v) ? insert (op aconvc) a
+          Free v => not (Term_Subst.Frees.defined fixed v) ? insert (op aconvc) a
         | _ => I)) th [];
   in fold Thm.forall_intr frees th end;
 
@@ -466,12 +468,27 @@
     val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th)
       handle TERM (msg, _) => raise THM (msg, 0, [th]);
 
-    val instT = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S)));
-    val instantiateT = Term_Subst.instantiateT (Term_Subst.TVars.table instT);
-    val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) =>
-      let val T' = instantiateT T
-      in (((a, i), T'), Thm.global_cterm_of thy (Free ((a, T')))) end);
-  in Thm.instantiate (map (apsnd (Thm.global_ctyp_of thy)) instT, inst) th end;
+    val cert = Thm.global_cterm_of thy;
+    val certT = Thm.global_ctyp_of thy;
+
+    val instT =
+      (prop, Term_Subst.TVars.empty) |-> (Term.fold_types o Term.fold_atyps)
+        (fn T => fn instT =>
+          (case T of
+            TVar (v as ((a, _), S)) =>
+              if Term_Subst.TVars.defined instT v then instT
+              else Term_Subst.TVars.update (v, TFree (a, S)) instT
+          | _ => instT));
+    val cinstT = Term_Subst.TVars.map (K certT) instT;
+    val cinst =
+      (prop, Term_Subst.Vars.empty) |-> Term.fold_aterms
+        (fn t => fn inst =>
+          (case t of
+            Var ((x, i), T) =>
+              let val T' = Term_Subst.instantiateT instT T
+              in Term_Subst.Vars.update (((x, i), T'), cert (Free ((x, T')))) inst end
+          | _ => inst));
+  in Thm.instantiate (Term_Subst.TVars.dest cinstT, Term_Subst.Vars.dest cinst) th end;
 
 fun unvarify_axiom thy = unvarify_global thy o Thm.axiom thy;
 

--- a/src/Pure/primitive_defs.ML	Sat Sep 04 14:46:32 2021 +0200
+++ b/src/Pure/primitive_defs.ML	Sat Sep 04 18:21:58 2021 +0200
@@ -37,7 +37,7 @@
     val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (\<equiv>)";
     val lhs = Envir.beta_eta_contract raw_lhs;
     val (head, args) = Term.strip_comb lhs;
-    val head_tfrees = Term.add_tfrees head [];
+    val head_tfrees = Term_Subst.add_tfrees head Term_Subst.TFrees.empty;
 
     fun check_arg (Bound _) = true
       | check_arg (Free (x, _)) = check_free_lhs x
@@ -52,7 +52,7 @@
       if check_free_rhs x orelse member (op aconv) args v then I
       else insert (op aconv) v | _ => I) rhs [];
     val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) =>
-      if check_tfree a orelse member (op =) head_tfrees (a, S) then I
+      if check_tfree a orelse Term_Subst.TFrees.defined head_tfrees (a, S) then I
       else insert (op =) v | _ => I)) rhs [];
   in
     if not (check_head head) then

--- a/src/Pure/theory.ML	Sat Sep 04 14:46:32 2021 +0200
+++ b/src/Pure/theory.ML	Sat Sep 04 18:21:58 2021 +0200
@@ -244,10 +244,10 @@
         [] => (item, map Logic.varifyT_global args)
       | vs => raise TYPE ("Illegal schematic type variable(s)", map TVar vs, []));
 
-    val lhs_vars = fold Term.add_tfreesT (snd lhs) [];
+    val lhs_vars = fold Term_Subst.add_tfreesT (snd lhs) Term_Subst.TFrees.empty;
     val rhs_extras =
       fold (fn (_, args) => args |> (fold o Term.fold_atyps) (fn TFree v =>
-        if member (op =) lhs_vars v then I else insert (op =) v)) rhs [];
+        if Term_Subst.TFrees.defined lhs_vars v then I else insert (op =) v)) rhs [];
     val _ =
       if null rhs_extras then ()
       else error ("Specification depends on extra type variables: " ^

--- a/src/Pure/variable.ML	Sat Sep 04 14:46:32 2021 +0200
+++ b/src/Pure/variable.ML	Sat Sep 04 18:21:58 2021 +0200
@@ -691,10 +691,10 @@
 
 fun focus_subgoal bindings i st =
   let
-    val all_vars = Thm.fold_terms Term.add_vars st [];
+    val all_vars = Thm.fold_terms Term_Subst.add_vars st Term_Subst.Vars.empty;
   in
-    fold (unbind_term o #1) all_vars #>
-    fold (declare_constraints o Var) all_vars #>
+    Term_Subst.Vars.fold (unbind_term o #1 o #1) all_vars #>
+    Term_Subst.Vars.fold (declare_constraints o Var o #1) all_vars #>
     focus_cterm bindings (Thm.cprem_of st i)
   end;