# HG changeset patch
# User wenzelm
# Date 1631002623 -7200
# Node ID cbbd08df65bd55570519abc77e1aef6160673a01
# Parent  38c01d7e9f5bedcf80e022c3ea2b7ba293aad833# Parent  9d9e7ed01dbbffd8f13098df0c38245303dc379b
merged

diff -r 38c01d7e9f5b -r cbbd08df65bd src/Doc/Implementation/Proof.thy
--- a/src/Doc/Implementation/Proof.thy	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Doc/Implementation/Proof.thy	Tue Sep 07 10:17:03 2021 +0200
@@ -101,7 +101,7 @@
   @{define_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
   @{define_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
   @{define_ML Variable.import: "bool -> thm list -> Proof.context ->
-  ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list)
+  ((ctyp Term_Subst.TVars.table * cterm Term_Subst.Vars.table) * thm list)
     * Proof.context"} \\
   @{define_ML Variable.focus: "binding list option -> term -> Proof.context ->
   ((string * (string * typ)) list * term) * Proof.context"} \\
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Doc/Typeclass_Hierarchy/Setup.thy
--- a/src/Doc/Typeclass_Hierarchy/Setup.thy	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Doc/Typeclass_Hierarchy/Setup.thy	Tue Sep 07 10:17:03 2021 +0200
@@ -6,7 +6,7 @@
 ML_file \<open>../more_antiquote.ML\<close>
 
 attribute_setup all =
-  \<open>Scan.succeed (Thm.rule_attribute [] (K Drule.forall_intr_vars))\<close>
+  \<open>Scan.succeed (Thm.rule_attribute [] (K Thm.forall_intr_vars))\<close>
   "quantified schematic vars"
 
 setup \<open>Config.put_global Printer.show_type_emphasis false\<close>
diff -r 38c01d7e9f5b -r cbbd08df65bd src/HOL/Analysis/metric_arith.ML
--- a/src/HOL/Analysis/metric_arith.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Analysis/metric_arith.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -24,8 +24,7 @@
 fun IF_UNSOLVED' tac i = IF_UNSOLVED (tac i)
 fun REPEAT' tac i = REPEAT (tac i)
 
-fun frees ct = Drule.cterm_add_frees ct []
-fun free_in v ct = member (op aconvc) (frees ct) v
+fun free_in v ct = member (op aconvc) (Misc_Legacy.cterm_frees ct) v
 
 (* build a cterm set with elements cts of type ty *)
 fun mk_ct_set ctxt ty =
diff -r 38c01d7e9f5b -r cbbd08df65bd src/HOL/Decision_Procs/ferrante_rackoff.ML
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -206,7 +206,7 @@
    val pcv = Simplifier.rewrite (put_simpset ss' ctxt);
    val postcv = Simplifier.rewrite (put_simpset ss ctxt);
    val nnf = K (nnf_conv ctxt then_conv postcv)
-   val qe_conv = Qelim.gen_qelim_conv ctxt pcv postcv pcv cons (Drule.cterm_add_frees tm [])
+   val qe_conv = Qelim.gen_qelim_conv ctxt pcv postcv pcv cons (Misc_Legacy.cterm_frees tm)
                   (isolate_conv ctxt) nnf
                   (fn vs => ferrack_conv ctxt (thy,{isolate_conv = isolate_conv ctxt,
                                                whatis = whatis, simpset = ss}) vs
diff -r 38c01d7e9f5b -r cbbd08df65bd src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Decision_Procs/langford.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -188,7 +188,7 @@
   in
     fn p =>
       Qelim.gen_qelim_conv ctxt pcv pcv dnfex_conv cons
-        (Drule.cterm_add_frees p []) (K Thm.reflexive) (K Thm.reflexive)
+        (Misc_Legacy.cterm_frees p) (K Thm.reflexive) (K Thm.reflexive)
         (K (basic_dloqe ctxt gst qe_bnds qe_nolb qe_noub gs)) p
   end;
 
diff -r 38c01d7e9f5b -r cbbd08df65bd src/HOL/Eisbach/eisbach_rule_insts.ML
--- a/src/HOL/Eisbach/eisbach_rule_insts.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Eisbach/eisbach_rule_insts.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -26,10 +26,10 @@
 
 fun add_thm_insts ctxt thm =
   let
-    val tyvars = Thm.fold_terms Term.add_tvars thm [];
+    val tyvars = Thm.fold_terms {hyps = false} Term.add_tvars thm [];
     val tyvars' = tyvars |> map (mk_term_type_internal o TVar);
 
-    val tvars = Thm.fold_terms Term.add_vars thm [];
+    val tvars = Thm.fold_terms {hyps = false} Term.add_vars thm [];
     val tvars' = tvars  |> map (Logic.mk_term o Var);
 
     val conj =
@@ -56,8 +56,8 @@
 
 fun instantiate_xis ctxt insts thm =
   let
-    val tyvars = Thm.fold_terms Term.add_tvars thm [];
-    val tvars = Thm.fold_terms Term.add_vars thm [];
+    val tyvars = Thm.fold_terms {hyps = false} Term.add_tvars thm [];
+    val tvars = Thm.fold_terms {hyps = false} Term.add_vars thm [];
 
     fun add_inst (xi, t) (Ts, ts) =
       (case AList.lookup (op =) tyvars xi of
diff -r 38c01d7e9f5b -r cbbd08df65bd src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -868,9 +868,11 @@
         then (RealArith.dest_ratconst (Thm.dest_arg1 tm), Thm.dest_arg tm)
         else raise Failure "substitutable_monomial"
     | \<^term>\<open>(+) :: real \<Rightarrow> _\<close>$_$_ =>
-         (substitutable_monomial (Drule.cterm_add_frees (Thm.dest_arg tm) fvs) (Thm.dest_arg1 tm)
+         (substitutable_monomial (merge (op aconvc) (fvs, Misc_Legacy.cterm_frees (Thm.dest_arg tm)))
+           (Thm.dest_arg1 tm)
            handle Failure _ =>
-            substitutable_monomial (Drule.cterm_add_frees (Thm.dest_arg1 tm) fvs) (Thm.dest_arg tm))
+            substitutable_monomial (merge (op aconvc) (fvs, Misc_Legacy.cterm_frees (Thm.dest_arg1 tm)))
+              (Thm.dest_arg tm))
     | _ => raise Failure "substitutable_monomial")
 
   fun isolate_variable v th =
diff -r 38c01d7e9f5b -r cbbd08df65bd src/HOL/Tools/Argo/argo_tactic.ML
--- a/src/HOL/Tools/Argo/argo_tactic.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Tools/Argo/argo_tactic.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -692,7 +692,7 @@
   thm
   |> instantiate_elim_rule
   |> Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion)
-  |> Drule.forall_intr_vars
+  |> Thm.forall_intr_vars
   |> Conv.fconv_rule (atomize_conv ctxt)
 
 
diff -r 38c01d7e9f5b -r cbbd08df65bd src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -830,7 +830,7 @@
                   (Variable.gen_all lthy
                     (Drule.rename_bvars'
                       (map (SOME o fst) xs')
-                      (Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
+                      (Thm.forall_intr_vars (case_thm RS (sel_def RS trans)))));
 
               val sel_thmss = @{map 3} (map oo make_sel_thm) xss' case_thms sel_defss;
 
diff -r 38c01d7e9f5b -r cbbd08df65bd src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Tools/Function/function_core.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -466,7 +466,7 @@
           forall_intr_rename (n, Thm.cterm_of lthy (Var (varmap (n, T), T)))) qs thm
       end
   in
-    ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy)
+    ((Rdef, map2 requantify intrs intrs_gen, Thm.forall_intr_vars elim_gen, induct), lthy)
   end
 
 fun define_graph (G_binding, G_type) fvar clauses RCss lthy =
@@ -809,7 +809,7 @@
     |> Thm.forall_intr (Thm.cterm_of ctxt' x)
     |> (fn it => Drule.compose (it, 2, wf_induct_rule))
     |> curry op RS (Thm.assume wfR')
-    |> forall_intr_vars
+    |> Thm.forall_intr_vars
     |> (fn it => it COMP allI)
     |> fold Thm.implies_intr hyps
     |> Thm.implies_intr wfR'
diff -r 38c01d7e9f5b -r cbbd08df65bd src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -300,7 +300,7 @@
     val th =
       th |> transform_elim_theorem
          |> zero_var_indexes
-         |> new_skolem ? forall_intr_vars
+         |> new_skolem ? Thm.forall_intr_vars
     val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
     val th = th |> Conv.fconv_rule (Object_Logic.atomize ctxt)
                 |> Meson.cong_extensionalize_thm ctxt
diff -r 38c01d7e9f5b -r cbbd08df65bd src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -870,8 +870,8 @@
     val (pats', _, ctxt3) = fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
     fun rewrite_pat (ct1, ct2) =
       (ct1, Thm.cterm_of ctxt3 (Pattern.rewrite_term thy pats' [] (Thm.term_of ct2)))
-    val t_insts' = map rewrite_pat t_insts
-    val intro'' = Thm.instantiate (T_insts, t_insts') intro
+    val t_insts' = map rewrite_pat (Term_Subst.Vars.dest t_insts)
+    val intro'' = Thm.instantiate (Term_Subst.TVars.dest T_insts, t_insts') intro
     val [intro'''] = Variable.export ctxt3 ctxt [intro'']
     val intro'''' =
       Simplifier.full_simplify
@@ -1162,7 +1162,9 @@
   let
      val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
      fun varify (t, (i, ts)) =
-       let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify_global [] t))
+       let
+         val t' = map_types (Logic.incr_tvar (i + 1))
+           (#2 (Type.varify_global Term_Subst.TFrees.empty t))
        in (maxidx_of_term t', t' :: ts) end
      val (i, cs') = List.foldr varify (~1, []) cs
      val (i', intr_ts') = List.foldr varify (i, []) intr_ts
diff -r 38c01d7e9f5b -r cbbd08df65bd src/HOL/Tools/Qelim/qelim.ML
--- a/src/HOL/Tools/Qelim/qelim.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Tools/Qelim/qelim.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -66,7 +66,7 @@
 
 fun standard_qelim_conv ctxt atcv ncv qcv p =
   let val pcv = pcv ctxt
-  in gen_qelim_conv ctxt pcv pcv pcv cons (Drule.cterm_add_frees p []) atcv ncv qcv p end
+  in gen_qelim_conv ctxt pcv pcv pcv cons (Misc_Legacy.cterm_frees p) atcv ncv qcv p end
 
 end;
 
diff -r 38c01d7e9f5b -r cbbd08df65bd src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -42,7 +42,7 @@
 
 fun atomize_thm ctxt thm =
   let
-    val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *)
+    val thm' = Thm.legacy_freezeT (Thm.forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *)
     val thm'' = Object_Logic.atomize ctxt (Thm.cprop_of thm')
   in
     @{thm equal_elim_rule1} OF [thm'', thm']
diff -r 38c01d7e9f5b -r cbbd08df65bd src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -255,7 +255,7 @@
   instantiate_elim #>
   norm_def #>
   Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion) #>
-  Drule.forall_intr_vars #>
+  Thm.forall_intr_vars #>
   Conv.fconv_rule (gen_normalize1_conv ctxt) #>
   (* Z3 4.3.1 silently normalizes "P --> Q --> R" to "P & Q --> R" *)
   Raw_Simplifier.rewrite_rule ctxt @{thms HOL.imp_conjL[symmetric, THEN eq_reflection]}
diff -r 38c01d7e9f5b -r cbbd08df65bd src/HOL/Tools/Transfer/transfer.ML
--- a/src/HOL/Tools/Transfer/transfer.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Tools/Transfer/transfer.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -696,7 +696,7 @@
     val rules = extra_rules @ get_transfer_raw ctxt
     val eq_rules = get_relator_eq_raw ctxt
     val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
-    val thm1 = Drule.forall_intr_vars thm
+    val thm1 = Thm.forall_intr_vars thm
     val instT =
       rev (Term.add_tvars (Thm.full_prop_of thm1) [])
       |> map (fn v as ((a, _), S) => (v, Thm.ctyp_of ctxt (TFree (a, S))))
@@ -731,7 +731,7 @@
     val rules = extra_rules @ get_transfer_raw ctxt
     val eq_rules = get_relator_eq_raw ctxt
     val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
-    val thm1 = Drule.forall_intr_vars thm
+    val thm1 = Thm.forall_intr_vars thm
     val instT =
       rev (Term.add_tvars (Thm.full_prop_of thm1) [])
       |> map (fn v as ((a, _), S) => (v, Thm.ctyp_of ctxt (TFree (a, S))))
diff -r 38c01d7e9f5b -r cbbd08df65bd src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Tools/choice_specification.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -99,7 +99,7 @@
     val frees = map snd props''
     val prop = myfoldr HOLogic.mk_conj (map fst props'')
 
-    val (vmap, prop_thawed) = Type.varify_global [] prop
+    val (vmap, prop_thawed) = Type.varify_global Term_Subst.TFrees.empty prop
     val thawed_prop_consts = collect_consts (prop_thawed, [])
     val (altcos, overloaded) = split_list cos
     val (names, sconsts) = split_list altcos
@@ -109,7 +109,7 @@
 
     fun proc_const c =
       let
-        val (_, c') = Type.varify_global [] c
+        val (_, c') = Type.varify_global Term_Subst.TFrees.empty c
         val (cname,ctyp) = dest_Const c'
       in
         (case filter (fn t =>
diff -r 38c01d7e9f5b -r cbbd08df65bd src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -131,7 +131,7 @@
       ||> Sign.restore_naming thy;
 
     val ivs = rev (Term.add_vars (Logic.varify_global (Old_Datatype_Prop.make_ind [descr])) []);
-    val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
+    val rvs = rev (Thm.fold_terms {hyps = false} Term.add_vars thm' []);
     val ivs1 = map Var (filter_out (fn (_, T) => \<^type_name>\<open>bool\<close> = tname_of (body_type T)) ivs);
     val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
 
diff -r 38c01d7e9f5b -r cbbd08df65bd src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/HOL/Tools/groebner.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -528,8 +528,7 @@
  fun simp_ex_conv ctxt =
    Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms(39)})
 
-fun frees t = Drule.cterm_add_frees t [];
-fun free_in v t = member op aconvc (frees t) v;
+fun free_in v t = member op aconvc (Misc_Legacy.cterm_frees t) v;
 
 val vsubst = let
  fun vsubst (t,v) tm =
@@ -737,7 +736,7 @@
       val T = Thm.typ_of_cterm x;
       val all = Thm.cterm_of ctxt (Const (\<^const_name>\<open>All\<close>, (T --> \<^typ>\<open>bool\<close>) --> \<^typ>\<open>bool\<close>))
     in Thm.apply all (Thm.lambda x p) end
-  val avs = Drule.cterm_add_frees tm []
+  val avs = Misc_Legacy.cterm_frees tm
   val P' = fold mk_forall avs tm
   val th1 = initial_conv ctxt (mk_neg P')
   val (evs,bod) = strip_exists(concl th1) in
@@ -796,7 +795,7 @@
    val mons = striplist(dest_binary ring_add_tm) t
   in member (op aconvc) mons v andalso
     forall (fn m => v aconvc m
-          orelse not(member (op aconvc) (Drule.cterm_add_frees m []) v)) mons
+          orelse not(member (op aconvc) (Misc_Legacy.cterm_frees m) v)) mons
   end
 
   fun isolate_variable vars tm =
@@ -851,7 +850,7 @@
  fun isolate_monomials vars tm =
  let
   val (cmons,vmons) =
-    List.partition (fn m => null (inter (op aconvc) vars (frees m)))
+    List.partition (fn m => null (inter (op aconvc) vars (Misc_Legacy.cterm_frees m)))
                    (striplist ring_dest_add tm)
   val cofactors = map (fn v => find_multipliers v vmons) vars
   val cnc = if null cmons then zero_tm
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/General/buffer.ML
--- a/src/Pure/General/buffer.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/General/buffer.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -9,8 +9,10 @@
   type T
   val empty: T
   val is_empty: T -> bool
+  val add: string -> T -> T
   val content: T -> string
-  val add: string -> T -> T
+  val build: (T -> T) -> T
+  val build_content: (T -> T) -> string
   val output: T -> (string -> unit) -> unit
   val markup: Markup.T -> (T -> T) -> T -> T
 end;
@@ -30,6 +32,9 @@
 
 fun content (Buffer xs) = implode (rev xs);
 
+fun build (f: T -> T) = f empty;
+fun build_content f = build f |> content;
+
 fun output (Buffer xs) out = List.app out (rev xs);
 
 end;
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/General/graph_display.ML
--- a/src/Pure/General/graph_display.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/General/graph_display.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -65,8 +65,9 @@
 fun build_graph entries =
   let
     val ident_names =
-      fold (fn ((ident, Node {name, ...}), _) => Symtab.update_new (ident, (name, ident)))
-        entries Symtab.empty;
+      Symtab.build
+        (entries |> fold (fn ((ident, Node {name, ...}), _) =>
+          Symtab.update_new (ident, (name, ident))));
     val the_key = the o Symtab.lookup ident_names;
   in
     Graph.empty
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/General/pretty.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -321,7 +321,7 @@
 (* special output *)
 
 (*symbolic markup -- no formatting*)
-fun symbolic prt =
+val symbolic =
   let
     fun out (Block ((bg, en), _, _, [], _)) = Buffer.add bg #> Buffer.add en
       | out (Block ((bg, en), consistent, indent, prts, _)) =
@@ -332,15 +332,15 @@
           Buffer.markup (Markup.break wd ind) (Buffer.add (output_spaces wd))
       | out (Break (true, _, _)) = Buffer.add (Output.output "\n")
       | out (Str (s, _)) = Buffer.add s;
-  in out prt Buffer.empty end;
+  in Buffer.build o out end;
 
 (*unformatted output*)
-fun unformatted prt =
+val unformatted =
   let
     fun out (Block ((bg, en), _, _, prts, _)) = Buffer.add bg #> fold out prts #> Buffer.add en
       | out (Break (_, wd, _)) = Buffer.add (output_spaces wd)
       | out (Str (s, _)) = Buffer.add s;
-  in out prt Buffer.empty end;
+  in Buffer.build o out end;
 
 
 (* output interfaces *)
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/General/table.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -19,18 +19,20 @@
   exception SAME
   exception UNDEF of key
   val empty: 'a table
+  val build: ('a table -> 'a table) -> 'a table
   val is_empty: 'a table -> bool
   val is_single: 'a table -> bool
   val map: (key -> 'a -> 'b) -> 'a table -> 'b table
   val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
   val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
+  val size: 'a table -> int
   val dest: 'a table -> (key * 'a) list
   val keys: 'a table -> key list
   val min: 'a table -> (key * 'a) option
   val max: 'a table -> (key * 'a) option
-  val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
   val exists: (key * 'a -> bool) -> 'a table -> bool
   val forall: (key * 'a -> bool) -> 'a table -> bool
+  val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
   val lookup_key: 'a table -> key -> (key * 'a) option
   val lookup: 'a table -> key -> 'a option
   val defined: 'a table -> key -> bool
@@ -60,6 +62,8 @@
   val insert_set: key -> set -> set
   val remove_set: key -> set -> set
   val make_set: key list -> set
+  val subset: set * set -> bool
+  val eq_set: set * set -> bool
 end;
 
 functor Table(Key: KEY): TABLE =
@@ -82,6 +86,8 @@
 
 val empty = Empty;
 
+fun build (f: 'a table -> 'a table) = f empty;
+
 fun is_empty Empty = true
   | is_empty _ = false;
 
@@ -118,6 +124,7 @@
           fold left (f p1 (fold mid (f p2 (fold right x))));
   in fold end;
 
+fun size tab = fold_table (fn _ => fn n => n + 1) tab 0;
 fun dest tab = fold_rev_table cons tab [];
 fun keys tab = fold_rev_table (cons o #1) tab [];
 
@@ -137,6 +144,20 @@
   | max (Branch3 (_, _, _, _, right)) = max right;
 
 
+(* exists and forall *)
+
+fun exists pred =
+  let
+    fun ex Empty = false
+      | ex (Branch2 (left, (k, x), right)) =
+          ex left orelse pred (k, x) orelse ex right
+      | ex (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
+          ex left orelse pred (k1, x1) orelse ex mid orelse pred (k2, x2) orelse ex right;
+  in ex end;
+
+fun forall pred = not o exists (not o pred);
+
+
 (* get_first *)
 
 fun get_first f =
@@ -164,9 +185,6 @@
           | some => some);
   in get end;
 
-fun exists pred = is_some o get_first (fn entry => if pred entry then SOME () else NONE);
-fun forall pred = not o exists (not o pred);
-
 
 (* lookup *)
 
@@ -424,7 +442,7 @@
 fun merge_list eq = join (fn _ => Library.merge eq);
 
 
-(* unit tables *)
+(* set operations *)
 
 type set = unit table;
 
@@ -432,6 +450,9 @@
 fun remove_set x : set -> set = delete_safe x;
 fun make_set entries = fold insert_set entries empty;
 
+fun subset (A: set, B: set) = forall (defined B o #1) A;
+fun eq_set (A: set, B: set) = size A = size B andalso subset (A, B);
+
 
 (* ML pretty-printing *)
 
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Isar/class.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -179,10 +179,8 @@
     val type_space = Proof_Context.type_space ctxt;
 
     val arities =
-      Symtab.empty
-      |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) =>
-           Symtab.map_default (class, []) (insert (op =) tyco)) arities)
-             (Sorts.arities_of algebra);
+      Symtab.build (Sorts.arities_of algebra |> Symtab.fold (fn (tyco, arities) =>
+        fold (fn (class, _) => Symtab.map_default (class, []) (insert (op =) tyco)) arities));
 
     fun prt_supersort class =
       Syntax.pretty_sort ctxt (Sign.minimize_sort thy (Sign.super_classes thy class));
@@ -610,7 +608,7 @@
           | SOME sorts =>
               fold2 (curry (Sorts.meet_sort algebra)) (Consts.typargs consts c_ty) sorts)
       | matchings _ = I;
-    val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
+    val tvartab = Vartab.build ((fold o fold_aterms) matchings ts)
       handle Sorts.CLASS_ERROR e => error (Sorts.class_error (Context.Proof ctxt) e);
     val inst = map_type_tvar
       (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Isar/code.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -960,7 +960,7 @@
         val _ = map (fn thm => if c = const_eqn thy thm then ()
           else error ("Wrong head of code equation,\nexpected constant "
             ^ string_of_const thy c ^ "\n" ^ Thm.string_of_thm_global thy thm)) thms;
-        fun tvars_of T = rev (Term.add_tvarsT T []);
+        val tvars_of = build_rev o Term.add_tvarsT;
         val vss = map (tvars_of o snd o head_eqn) thms;
         fun inter_sorts vs =
           fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Isar/generic_target.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -95,8 +95,10 @@
     val u = fold_rev lambda term_params rhs';
     val global_rhs = singleton (Variable.polymorphic thy_ctxt) u;
 
+    val type_tfrees = Term_Subst.TFrees.build (Term_Subst.add_tfreesT (Term.fastype_of u));
     val extra_tfrees =
-      subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []);
+      build_rev (u |> (Term.fold_types o Term.fold_atyps)
+        (fn TFree v => not (Term_Subst.TFrees.defined type_tfrees v) ? insert (op =) v | _ => I));
     val type_params = map (Logic.mk_type o TFree) extra_tfrees;
   in (global_rhs, (extra_tfrees, (type_params, term_params))) end;
 
@@ -259,8 +261,11 @@
 
     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.build (Term_Subst.add_tfreesT T #> fold (Term_Subst.add_tfreesT o #2) xs);
+    val extra_tfrees =
+      build_rev (rhs |> (Term.fold_types o Term.fold_atyps)
+        (fn TFree v => not (Term_Subst.TFrees.defined type_tfrees v) ? insert (op =) v | _ => I));
     val mx' = check_mixfix lthy (b, extra_tfrees) mx;
 
     val type_params = map (Logic.mk_type o TFree) extra_tfrees;
@@ -302,8 +307,8 @@
     val asms' = map (rewrite_rule ctxt (Drule.norm_hhf_eqs @ defs)) asms;
 
     (*export fixes*)
-    val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
-    val frees = map Free (Thm.fold_terms Term.add_frees th' []);
+    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 (th'' :: vs) =
       (th' :: map (Drule.mk_term o Thm.cterm_of ctxt) (map Logic.mk_type tfrees @ frees))
       |> Variable.export ctxt thy_ctxt
@@ -318,8 +323,8 @@
       |>> map Logic.dest_type;
 
     val instT =
-      fold2 (fn a => fn b => (case a of TVar v => Term_Subst.TVars.add (v, b) | _ => I))
-        tvars tfrees Term_Subst.TVars.empty;
+      Term_Subst.TVars.build (fold2 (fn a => fn b =>
+        (case a of TVar v => Term_Subst.TVars.add (v, b) | _ => I)) tvars tfrees);
     val cinstT = Term_Subst.TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt T)) instT [];
     val cinst =
       map_filter
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Isar/method.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -118,7 +118,7 @@
 
 fun insert_tac _ [] _ = all_tac
   | insert_tac ctxt facts i =
-      EVERY (map (fn r => resolve_tac ctxt [Drule.forall_intr_vars r COMP_INCR revcut_rl] i) facts);
+      EVERY (map (fn r => resolve_tac ctxt [Thm.forall_intr_vars r COMP_INCR revcut_rl] i) facts);
 
 fun insert thms =
   CONTEXT_METHOD (fn _ => fn (ctxt, st) =>
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Isar/obtain.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -103,8 +103,11 @@
 
 fun mk_all_internal ctxt (y, z) t =
   let
+    val frees =
+      Term_Subst.Frees.build (t |> 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,16 @@
     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))));
+      Term_Subst.TVars.build
+        (params |> 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' =
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Isar/overloading.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -76,7 +76,7 @@
               then SOME (ty', apply_subst t') else NONE
           | NONE => NONE)
         | _ => NONE) t;
-    val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty;
+    val improvements = Vartab.build ((fold o fold_aterms) accumulate_improvements ts);
     val ts' =
       ts
       |> (map o map_types) (Envir.subst_type improvements)
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -724,10 +724,10 @@
       end;
 
     val env =
-      (fold o fold_atyps)
+      Vartab.build (tys |> (fold o fold_atyps)
         (fn TFree (x, S) => constraint ((x, ~1), S)
           | TVar v => constraint v
-          | _ => I) tys Vartab.empty;
+          | _ => I));
 
     fun get_sort xi raw_S =
       if xi = dummy_var then
@@ -1269,8 +1269,8 @@
         NONE => Inttab.empty
       | SOME ctxt0 =>
           let val cases0 = cases_of ctxt0 in
-            Name_Space.fold_table (fn (a, _) => Inttab.insert_set (serial_of cases0 a))
-              cases0 Inttab.empty
+            Inttab.build (cases0 |> Name_Space.fold_table (fn (a, _) =>
+              Inttab.insert_set (serial_of cases0 a)))
           end);
      val cases = cases_of ctxt;
   in
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Isar/specification.ML	Tue Sep 07 10:17:03 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.Frees.build (Term_Subst.add_frees lhs'))) [(x, T)];
   in ((lhs, (def_name, th')), lthy5) end;
 
 val definition' = gen_def check_spec_open (K I);
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/Isar/subgoal.ML
--- a/src/Pure/Isar/subgoal.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Isar/subgoal.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -58,7 +58,7 @@
     val ((_, inst), ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
     val schematic_terms = Term_Subst.Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt3 t)) inst [];
 
-    val schematics = (schematic_types, schematic_terms);
+    val schematics = (Term_Subst.TVars.dest schematic_types, schematic_terms);
     val asms' = map (Thm.instantiate_cterm schematics) asms;
     val concl' = Thm.instantiate_cterm schematics concl;
     val (prems, context) = Assumption.add_assumes asms' ctxt3;
@@ -88,15 +88,15 @@
     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 vars = rev (Term.add_vars prop []);
+    val concl_vars = Term_Subst.Vars.build (Term_Subst.add_vars (Logic.strip_imp_concl prop));
+    val vars = build_rev (Term.add_vars prop);
     val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
 
     fun var_inst v y =
       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;
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/PIDE/document.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -490,15 +490,15 @@
 
     val versions' = fold delete_version version_ids versions;
     val commands' =
-      (versions', Inttab.empty) |->
+      Inttab.build (versions' |>
         Inttab.fold (fn (_, version) => nodes_of version |>
           String_Graph.fold (fn (_, (node, _)) => node |>
             iterate_entries (fn ((_, command_id), _) =>
-              SOME o Inttab.insert (K true) (command_id, the_command state command_id))));
+              SOME o Inttab.insert (K true) (command_id, the_command state command_id)))));
     val blobs' =
-      (commands', Symtab.empty) |->
+      Symtab.build (commands' |>
         Inttab.fold (fn (_, (_, blobs, _, _)) => blobs |>
-          fold (fn Exn.Res {digest = SOME b, ...} => Symtab.update (b, the_blob state b) | _ => I));
+          fold (fn Exn.Res {digest = SOME b, ...} => Symtab.update (b, the_blob state b) | _ => I)));
 
   in (versions', blobs', commands', execution) end);
 
@@ -815,7 +815,7 @@
     val nodes = nodes_of new_version;
     val required = make_required nodes;
     val required0 = make_required (nodes_of old_version);
-    val edited = fold (fn (name, _) => Symtab.update (name, ())) edits Symtab.empty;
+    val edited = Symtab.build (edits |> fold (fn (name, _) => Symtab.update (name, ())));
 
     val updated = timeit "Document.update" (fn () =>
       nodes |> String_Graph.schedule
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/PIDE/resources.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -118,8 +118,8 @@
     (fn _ =>
       ({session_positions = sort_by #1 (map (apsnd make_entry) session_positions),
         session_directories =
-          fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir))
-            session_directories Symtab.empty,
+          Symtab.build (session_directories |> fold_rev (fn (dir, name) =>
+            Symtab.cons_list (name, Path.explode dir))),
         session_chapters = Symtab.make session_chapters,
         bibtex_entries = Symtab.make bibtex_entries,
         timings = make_timings command_timings,
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/PIDE/xml.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -110,7 +110,7 @@
         Elem (_, ts) => fold add_content ts
       | Text s => Buffer.add s));
 
-fun content_of body = Buffer.empty |> fold add_content body |> Buffer.content;
+val content_of = Buffer.build_content o fold add_content;
 
 
 (* trim blanks *)
@@ -164,9 +164,9 @@
   else (enclose "<" ">" (elem name atts), enclose "</" ">" name);
 
 
-(* output *)
+(* output content *)
 
-fun buffer_of depth tree =
+fun content_depth depth =
   let
     fun traverse _ (Elem ((name, atts), [])) =
           Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>"
@@ -177,12 +177,11 @@
       | traverse _ (Text s) = Buffer.add (text s)
     and traverse_body 0 _ = Buffer.add "..."
       | traverse_body d ts = fold (traverse (d - 1)) ts;
-  in Buffer.empty |> traverse depth tree end;
+  in Buffer.build_content o traverse depth end;
 
-val string_of = Buffer.content o buffer_of ~1;
+val string_of = content_depth ~1;
 
-fun pretty depth tree =
-  Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
+fun pretty depth tree = Pretty.str (content_depth (Int.max (0, depth)) tree);
 
 val _ = ML_system_pp (fn depth => fn _ => Pretty.to_polyml o pretty (FixedInt.toInt depth));
 
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/PIDE/yxml.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -85,7 +85,7 @@
 
 (* output *)
 
-fun string_of_body body = Buffer.empty |> fold (traverse Buffer.add) body |> Buffer.content;
+val string_of_body = Buffer.build_content o fold (traverse Buffer.add);
 val string_of = string_of_body o single;
 
 fun write_body path body =
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Proof/extraction.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -123,8 +123,8 @@
 
 fun msg d s = writeln (Symbol.spaces d ^ s);
 
-fun vars_of t = map Var (rev (Term.add_vars t []));
-fun frees_of t = map Free (rev (Term.add_frees t []));
+fun vars_of t = map Var (build_rev (Term.add_vars t));
+fun frees_of t = map Free (build_rev (Term.add_frees t));
 fun vfs_of t = vars_of t @ frees_of t;
 
 val mkabs = fold_rev (fn v => fn t => Abs ("x", fastype_of v, abstract_over (v, t)));
@@ -385,7 +385,7 @@
     val atyps = fold_types (fold_atyps (insert (op =))) (Thm.prop_of thm) [];
     val Ts = map_filter (fn ((v, i), _) => if member (op =) vs v then
         SOME (TVar (("'" ^ v, i), [])) else NONE)
-      (rev (Term.add_vars prop' []));
+      (build_rev (Term.add_vars prop'));
     val cs = maps (fn T => map (pair T) S) Ts;
     val constraints' = map Logic.mk_of_class cs;
     fun typ_map T = Type.strip_sorts
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/Proof/proof_checker.ML
--- a/src/Pure/Proof/proof_checker.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Proof/proof_checker.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -16,7 +16,7 @@
 (***** construct a theorem out of a proof term *****)
 
 fun lookup_thm thy =
-  let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy true) Symtab.empty in
+  let val tab = Symtab.build (Global_Theory.all_thms_of thy true |> fold_rev Symtab.update) in
     fn s =>
       (case Symtab.lookup tab s of
         NONE => error ("Unknown theorem " ^ quote s)
@@ -76,12 +76,12 @@
 
         fun thm_of_atom thm Ts =
           let
-            val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
-            val (fmap, thm') = Thm.varifyT_global' [] thm;
+            val tvars = build_rev (Term.add_tvars (Thm.full_prop_of thm));
+            val (fmap, thm') = Thm.varifyT_global' Term_Subst.TFrees.empty thm;
             val ctye =
               (tvars @ map (fn ((_, S), ixn) => (ixn, S)) fmap ~~ map (Thm.global_ctyp_of thy) Ts);
           in
-            Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
+            Thm.instantiate (ctye, []) (Thm.forall_intr_vars (Thm.forall_intr_frees thm'))
           end;
 
         fun thm_of _ _ (PThm ({name, prop = prop', types = SOME Ts, ...}, _)) =
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -249,7 +249,7 @@
           if member (op =) defs s then
             let
               val vs = vars_of prop;
-              val tvars = Term.add_tvars prop [] |> rev;
+              val tvars = build_rev (Term.add_tvars prop);
               val (_, rhs) = Logic.dest_equals (Logic.strip_imp_concl prop);
               val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
                 (fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
@@ -291,11 +291,11 @@
 fun elim_vars mk_default prf =
   let
     val prop = Proofterm.prop_of prf;
-    val tv = Term.add_vars prop [];
-    val tf = Term.add_frees prop [];
+    val tv = Term_Subst.Vars.build (Term_Subst.add_vars prop);
+    val tf = Term_Subst.Frees.build (Term_Subst.add_frees prop);
 
-    fun hidden_variable (Var v) = not (member (op =) tv v)
-      | hidden_variable (Free f) = not (member (op =) tf f)
+    fun hidden_variable (Var v) = not (Term_Subst.Vars.defined tv v)
+      | hidden_variable (Free f) = not (Term_Subst.Frees.defined tf f)
       | hidden_variable _ = false;
 
     fun mk_default' T =
@@ -303,8 +303,8 @@
 
     fun elim_varst (t $ u) = elim_varst t $ elim_varst u
       | elim_varst (Abs (s, T, t)) = Abs (s, T, elim_varst t)
-      | elim_varst (t as Free (x, T)) = if member (op =) tf (x, T) then t else mk_default' T
-      | elim_varst (t as Var (xi, T)) = if member (op =) tv (xi, T) then t else mk_default' T
+      | elim_varst (t as Free (x, T)) = if Term_Subst.Frees.defined tf (x, T) then t else mk_default' T
+      | elim_varst (t as Var (xi, T)) = if Term_Subst.Vars.defined tv (xi, T) then t else mk_default' T
       | elim_varst t = t;
   in
     Proofterm.map_proof_terms (fn t =>
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Syntax/ast.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -158,7 +158,7 @@
           end
       | _ => (ast, []));
   in
-    SOME (mtch head pat Symtab.empty, args) handle NO_MATCH => NONE
+    SOME (Symtab.build (mtch head pat), args) handle NO_MATCH => NONE
   end;
 
 
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/System/options.ML
--- a/src/Pure/System/options.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/System/options.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -156,8 +156,8 @@
 fun encode (Options tab) =
   let
     val opts =
-      (tab, []) |-> Symtab.fold (fn (name, {pos, typ, value}) =>
-        cons (Position.properties_of pos, (name, (typ, value))));
+      build (tab |> Symtab.fold (fn (name, {pos, typ, value}) =>
+        cons (Position.properties_of pos, (name, (typ, value)))));
     open XML.Encode;
   in list (pair properties (pair string (pair string string))) opts end;
 
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Thy/export_theory.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -78,7 +78,7 @@
           SOME goal => Thm.prems_of goal
         | NONE => raise Fail ("Cannot unfold locale " ^ quote loc))
       end;
-    val typargs = rev (fold Term.add_tfrees (map (Free o #1) args @ axioms) []);
+    val typargs = build_rev (fold Term.add_tfrees (map (Free o #1) args @ axioms));
   in {typargs = typargs, args = args, axioms = axioms} end;
 
 fun get_locales thy =
@@ -148,8 +148,8 @@
        {props = pos_properties pos,
         name = name,
         rough_classification = rough_classification,
-        typargs = rev (fold Term.add_tfrees spec []),
-        args = rev (fold Term.add_frees spec []),
+        typargs = build_rev (fold Term.add_tfrees spec),
+        args = build_rev (fold Term.add_frees spec),
         terms = map (fn t => (t, Term.type_of t)) (take (length terms) spec),
         rules = drop (length terms) spec}
       end;
@@ -172,7 +172,7 @@
         val parent_spaces = map get_space parents;
         val space = get_space thy;
       in
-        (decls, []) |-> fold (fn (name, decl) =>
+        build (decls |> fold (fn (name, decl) =>
           if exists (fn space => Name_Space.declared space name) parent_spaces then I
           else
             (case export name decl of
@@ -181,7 +181,7 @@
                 let
                   val i = #serial (Name_Space.the_entry space name);
                   val body = if enabled then make_body () else [];
-                in cons (i, XML.Elem (entity_markup space name, body)) end))
+                in cons (i, XML.Elem (entity_markup space name, body)) end)))
         |> sort (int_ord o apply2 #1) |> map #2
         |> export_body thy export_name
       end;
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Tools/find_consts.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -90,7 +90,7 @@
           let val qty = make_pattern arg; in
             fn (_, (ty, _)) =>
               let
-                val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
+                val tye = Vartab.build (Sign.typ_match thy (qty, ty));
                 val sub_size =
                   Vartab.fold (fn (_, (_, t)) => fn n => Term.size_of_typ t + n) tye 0;
               in SOME sub_size end handle Type.TYPE_MATCH => NONE
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -52,13 +52,13 @@
 fun error_var msg (xi, pos) =
   error (msg ^ quote (Term.string_of_vname xi) ^ Position.here pos);
 
-fun the_sort tvars (xi, pos) : sort =
-  (case AList.lookup (op =) tvars xi of
+fun the_sort tvars (ai, pos) : sort =
+  (case Term_Subst.TVars.get_first (fn ((bi, S), ()) => if ai = bi then SOME S else NONE) tvars of
     SOME S => S
-  | NONE => error_var "No such type variable in theorem: " (xi, pos));
+  | NONE => error_var "No such type variable in theorem: " (ai, pos));
 
 fun the_type vars (xi, pos) : typ =
-  (case AList.lookup (op =) vars xi of
+  (case Vartab.lookup vars xi of
     SOME T => T
   | NONE => error_var "No such variable in theorem: " (xi, pos));
 
@@ -71,17 +71,23 @@
     else error_var "Bad sort for instantiation of type variable: " (xi, pos)
   end;
 
-fun make_instT f v =
+fun make_instT f (tvars: Term_Subst.TVars.set) =
   let
-    val T = TVar v;
-    val T' = f T;
-  in if T = T' then NONE else SOME (v, T') end;
+    fun add v =
+      let
+        val T = TVar v;
+        val T' = f T;
+      in if T = T' then I else cons (v, T') end;
+  in Term_Subst.TVars.fold (add o #1) tvars [] end;
 
-fun make_inst f v =
+fun make_inst f vars =
   let
-    val t = Var v;
-    val t' = f t;
-  in if t aconv t' then NONE else SOME (v, t') end;
+    fun add v =
+      let
+        val t = Var v;
+        val t' = f t;
+      in if t aconv t' then I else cons (v, t') end;
+  in fold add vars [] end;
 
 fun read_terms ss Ts ctxt =
   let
@@ -92,7 +98,7 @@
       |> Syntax.check_terms ctxt'
       |> Variable.polymorphic ctxt';
     val Ts' = map Term.fastype_of ts';
-    val tyenv = fold (Sign.typ_match (Proof_Context.theory_of ctxt)) (Ts ~~ Ts') Vartab.empty;
+    val tyenv = Vartab.build (fold (Sign.typ_match (Proof_Context.theory_of ctxt)) (Ts ~~ Ts'));
     val tyenv' = Vartab.fold (fn (xi, (S, T)) => cons ((xi, S), T)) tyenv [];
   in ((ts', tyenv'), ctxt') end;
 
@@ -109,19 +115,21 @@
     val (type_insts, term_insts) =
       List.partition (fn (((x, _), _), _) => String.isPrefix "'" x) raw_insts;
 
-    val tvars = Thm.fold_terms Term.add_tvars thm [];
-    val vars = Thm.fold_terms Term.add_vars thm [];
+    val tvars = Term_Subst.TVars.build (Thm.fold_terms {hyps = false} Term_Subst.add_tvars thm);
+    val vars = Term_Subst.Vars.build (Thm.fold_terms {hyps = false} Term_Subst.add_vars thm);
 
     (*eigen-context*)
     val (_, ctxt1) = ctxt
-      |> fold (Variable.declare_internal o Logic.mk_type o TVar) tvars
-      |> fold (Variable.declare_internal o Var) vars
+      |> Term_Subst.TVars.fold (Variable.declare_internal o Logic.mk_type o TVar o #1) tvars
+      |> Term_Subst.Vars.fold (Variable.declare_internal o Var o #1) vars
       |> Proof_Context.add_fixes_cmd raw_fixes;
 
     (*explicit type instantiations*)
     val instT1 =
       Term_Subst.instantiateT (Term_Subst.TVars.table (map (read_type ctxt1 tvars) type_insts));
-    val vars1 = map (apsnd instT1) vars;
+    val vars1 =
+      Vartab.build (vars |> Term_Subst.Vars.fold (fn ((v, T), ()) =>
+        Vartab.insert (K true) (v, instT1 T)));
 
     (*term instantiations*)
     val (xs, ss) = split_list term_insts;
@@ -130,15 +138,15 @@
 
     (*implicit type instantiations*)
     val instT2 = Term_Subst.instantiateT (Term_Subst.TVars.table inferred);
-    val vars2 = map (apsnd instT2) vars1;
+    val vars2 = Vartab.fold (fn (v, T) => cons (v, instT2 T)) vars1 [];
     val inst2 =
       Term_Subst.instantiate (Term_Subst.TVars.empty,
-        fold2 (fn (xi, _) => fn t => Term_Subst.Vars.add ((xi, Term.fastype_of t), t))
-          xs ts Term_Subst.Vars.empty)
+        Term_Subst.Vars.build
+          (fold2 (fn (xi, _) => fn t => Term_Subst.Vars.add ((xi, Term.fastype_of t), t)) xs ts))
       #> Envir.beta_norm;
 
-    val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars;
-    val inst_vars = map_filter (make_inst inst2) vars2;
+    val inst_tvars = make_instT (instT2 o instT1) tvars;
+    val inst_vars = make_inst inst2 vars2;
   in ((inst_tvars, inst_vars), ctxt2) end;
 
 end;
@@ -166,8 +174,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 (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @
-      zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args;
+      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;
   in where_rule ctxt insts fixes thm end;
 
 fun read_instantiate ctxt insts xs =
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/consts.ML
--- a/src/Pure/consts.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/consts.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -227,8 +227,8 @@
     val declT = type_scheme consts c;
     val args = typargs consts (c, declT);
     val inst =
-      fold2 (fn a => fn T => Term_Subst.TVars.add (Term.dest_TVar a, T))
-        args Ts Term_Subst.TVars.empty
+      Term_Subst.TVars.build
+        (fold2 (fn a => fn T => Term_Subst.TVars.add (Term.dest_TVar a, T)) args Ts)
       handle ListPair.UnequalLengths => raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]);
   in declT |> Term_Subst.instantiateT inst end;
 
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/context.ML
--- a/src/Pure/context.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/context.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -466,10 +466,10 @@
 end;
 
 fun theory_data_size thy =
-  (data_of thy, []) |-> Datatab.fold_rev (fn (k, _) =>
+  build (data_of thy |> Datatab.fold_rev (fn (k, _) =>
     (case Theory_Data.obj_size k thy of
       NONE => I
-    | SOME n => (cons (invoke_pos k, n))));
+    | SOME n => (cons (invoke_pos k, n)))));
 
 
 
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/defs.ML
--- a/src/Pure/defs.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/defs.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -85,13 +85,13 @@
 
 fun disjoint_args (Ts, Us) =
   not (Type.could_unifys (Ts, Us)) orelse
-    ((Type.raw_unifys (Ts, map (Logic.incr_tvar (maxidx_of_typs Ts + 1)) Us) Vartab.empty; false)
+    ((Vartab.build (Type.raw_unifys (Ts, map (Logic.incr_tvar (maxidx_of_typs Ts + 1)) Us)); false)
       handle Type.TUNIFY => true);
 
 fun match_args (Ts, Us) =
   if Type.could_matches (Ts, Us) then
     Option.map Envir.subst_type
-      (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE)
+      (SOME (Vartab.build (Type.raw_matches (Ts, Us))) handle Type.TYPE_MATCH => NONE)
   else NONE;
 
 
@@ -148,10 +148,10 @@
         NONE => false
       | SOME {specs, ...} => Inttab.defined specs i));
   in
-    (defs, []) |-> Itemtab.fold (fn (c, {specs, ...}) =>
+    build (defs |> Itemtab.fold (fn (c, {specs, ...}) =>
       specs |> Inttab.fold (fn (i, spec) =>
         if #1 c = Const andalso is_some (#def spec) andalso not (prev_spec c i)
-        then cons (#2 c, the (#def spec)) else I))
+        then cons (#2 c, the (#def spec)) else I)))
   end;
 
 val empty = Defs Itemtab.empty;
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/drule.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -14,7 +14,6 @@
   val strip_imp_concl: cterm -> cterm
   val cprems_of: thm -> cterm list
   val forall_intr_list: cterm list -> thm -> thm
-  val forall_intr_vars: thm -> thm
   val forall_elim_list: cterm list -> thm -> thm
   val lift_all: Proof.context -> cterm -> thm -> thm
   val implies_elim_list: thm -> thm list -> thm
@@ -89,8 +88,6 @@
   val mk_term: cterm -> thm
   val dest_term: thm -> cterm
   val cterm_rule: (thm -> thm) -> cterm -> cterm
-  val cterm_add_frees: cterm -> cterm list -> cterm list
-  val cterm_add_vars: cterm -> cterm list -> cterm list
   val dummy_thm: thm
   val free_dummy_thm: thm
   val is_sort_constraint: term -> bool
@@ -165,9 +162,6 @@
 (*Generalization over a list of variables*)
 val forall_intr_list = fold_rev Thm.forall_intr;
 
-(*Generalization over Vars -- canonical order*)
-fun forall_intr_vars th = fold Thm.forall_intr (Thm.add_vars th []) th;
-
 fun outer_params t =
   let val vs = Term.strip_all_vars t
   in Name.variant_list [] (map (Name.clean o #1) vs) ~~ map #2 vs end;
@@ -185,11 +179,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))));
+      Term_Subst.Vars.build (th |> (Thm.fold_terms {hyps = false} 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;
 
@@ -212,17 +213,17 @@
         val (instT, inst) =
           Term_Subst.zero_var_indexes_inst Name.context (map Thm.full_prop_of ths);
 
-        val tvars = fold Thm.add_tvars ths [];
-        fun the_tvar v = the (find_first (fn cT => v = dest_TVar (Thm.typ_of cT)) tvars);
+        val tvars = fold Thm.add_tvars ths Term_Subst.TVars.empty;
+        val the_tvar = the o Term_Subst.TVars.lookup tvars;
         val instT' =
-          (instT, []) |-> Term_Subst.TVars.fold (fn (v, TVar (b, _)) =>
-            cons (v, Thm.rename_tvar b (the_tvar v)));
+          build (instT |> Term_Subst.TVars.fold (fn (v, TVar (b, _)) =>
+            cons (v, Thm.rename_tvar b (the_tvar v))));
 
-        val vars = fold (Thm.add_vars o Thm.instantiate (instT', [])) ths [];
-        fun the_var v = the (find_first (fn ct => v = dest_Var (Thm.term_of ct)) vars);
+        val vars = fold (Thm.add_vars o Thm.instantiate (instT', [])) ths Term_Subst.Vars.empty;
+        val the_var = the o Term_Subst.Vars.lookup vars;
         val inst' =
-          (inst, []) |-> Term_Subst.Vars.fold (fn (v, Var (b, _)) =>
-            cons (v, Thm.var (b, Thm.ctyp_of_cterm (the_var v))));
+          build (inst |> Term_Subst.Vars.fold (fn (v, Var (b, _)) =>
+            cons (v, Thm.var (b, Thm.ctyp_of_cterm (the_var v)))));
       in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (instT', inst')) ths end;
 
 val zero_var_indexes = singleton zero_var_indexes_list;
@@ -610,9 +611,6 @@
 
 fun cterm_rule f = dest_term o f o mk_term;
 
-val cterm_add_frees = Thm.add_frees o mk_term;
-val cterm_add_vars = Thm.add_vars o mk_term;
-
 val dummy_thm = mk_term (certify Term.dummy_prop);
 val free_dummy_thm = Thm.tag_free_dummy dummy_thm;
 
@@ -788,7 +786,7 @@
 
 fun infer_instantiate' ctxt args th =
   let
-    val vars = rev (Term.add_vars (Thm.full_prop_of th) []);
+    val vars = build_rev (Term.add_vars (Thm.full_prop_of th));
     val args' = zip_options vars args
       handle ListPair.UnequalLengths =>
         raise THM ("infer_instantiate': more instantiations than variables in thm", 0, [th]);
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/envir.ML
--- a/src/Pure/envir.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/envir.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -395,7 +395,7 @@
 (** expand defined atoms -- with local beta reduction **)
 
 fun expand_atom T (U, u) =
-  subst_term_types (Type.raw_match (U, T) Vartab.empty) u
+  subst_term_types (Vartab.build (Type.raw_match (U, T))) u
     handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
 
 fun expand_term get =
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/facts.ML
--- a/src/Pure/facts.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/facts.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -217,7 +217,8 @@
 fun consolidate facts =
   let
     val unfinished =
-      (facts, []) |-> fold_static_lazy (fn (_, ths) => if Lazy.is_finished ths then I else cons ths);
+      build (facts |> fold_static_lazy (fn (_, ths) =>
+        if Lazy.is_finished ths then I else cons ths));
     val _ = Lazy.consolidate unfinished;
   in facts end;
 
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/global_theory.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -124,8 +124,8 @@
 fun lookup_thm_id thy =
   let
     val theories =
-      fold (fn thy' => Symtab.update (Context.theory_long_name thy', lazy_thm_names thy'))
-        (Theory.nodes_of thy) Symtab.empty;
+      Symtab.build (Theory.nodes_of thy |> fold (fn thy' =>
+        Symtab.update (Context.theory_long_name thy', lazy_thm_names thy')));
     fun lookup (thm_id: Proofterm.thm_id) =
       (case Symtab.lookup theories (#theory_name thm_id) of
         NONE => NONE
@@ -170,8 +170,8 @@
 fun transfer_theories thy =
   let
     val theories =
-      fold (fn thy' => Symtab.update (Context.theory_name thy', thy'))
-        (Theory.nodes_of thy) Symtab.empty;
+      Symtab.build (Theory.nodes_of thy |> fold (fn thy' =>
+        Symtab.update (Context.theory_name thy', thy')));
     fun transfer th =
       Thm.transfer (the_default thy (Symtab.lookup theories (Thm.theory_name th))) th;
   in transfer end;
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/goal.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -116,30 +116,34 @@
     val assms = Assumption.all_assms_of ctxt;
     val As = map Thm.term_of assms;
 
-    val xs = map Free (fold Term.add_frees (prop :: As) []);
-    val fixes = map (Thm.cterm_of ctxt) xs;
+    val frees = Term_Subst.Frees.build (fold Term_Subst.add_frees (prop :: As));
+    val xs = Term_Subst.Frees.fold_rev (cons o Thm.cterm_of ctxt o Free o #1) frees [];
 
-    val tfrees = fold Term.add_tfrees (prop :: As) [];
-    val tfrees_set = fold (Symtab.insert_set o #1) tfrees Symtab.empty;
-    val instT = map (fn (a, S) => (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S)))) tfrees;
+    val tfrees = Term_Subst.TFrees.build (fold Term_Subst.add_tfrees (prop :: As));
+    val Ts = Symtab.build (Term_Subst.TFrees.fold (Symtab.insert_set o #1 o #1) tfrees);
+    val instT =
+      build (tfrees |> Term_Subst.TFrees.fold (fn ((a, S), ()) =>
+        cons (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S)))));
 
     val global_prop =
-      Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop)))
+      Logic.list_implies (As, prop)
+      |> Term_Subst.Frees.fold_rev (Logic.all o Free o #1) frees
+      |> Logic.varify_types_global
       |> Thm.cterm_of ctxt
       |> Thm.weaken_sorts' ctxt;
     val global_result = result |> Future.map
       (Drule.flexflex_unique (SOME ctxt) #>
         Drule.implies_intr_list assms #>
-        Drule.forall_intr_list fixes #>
+        Drule.forall_intr_list xs #>
         Thm.adjust_maxidx_thm ~1 #>
-        Thm.generalize (tfrees_set, Symtab.empty) 0 #>
+        Thm.generalize (Ts, Symtab.empty) 0 #>
         Thm.strip_shyps #>
         Thm.solve_constraints);
     val local_result =
       Thm.future global_result global_prop
       |> Thm.close_derivation \<^here>
       |> Thm.instantiate (instT, [])
-      |> Drule.forall_elim_list fixes
+      |> Drule.forall_elim_list xs
       |> fold (Thm.elim_implies o Thm.assume) assms
       |> Thm.solve_constraints;
   in local_result end;
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/library.ML
--- a/src/Pure/library.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/library.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -51,6 +51,8 @@
   val forall: ('a -> bool) -> 'a list -> bool
 
   (*lists*)
+  val build: ('a list -> 'a list) -> 'a list
+  val build_rev: ('a list -> 'a list) -> 'a list
   val single: 'a -> 'a list
   val the_single: 'a list -> 'a
   val singleton: ('a list -> 'b list) -> 'a -> 'b
@@ -301,6 +303,9 @@
 
 (** lists **)
 
+fun build (f: 'a list -> 'a list) = f [];
+fun build_rev f = build f |> rev;
+
 fun single x = [x];
 
 fun the_single [x] = x
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/more_thm.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -25,9 +25,8 @@
   structure Thmtab: TABLE
   val eq_ctyp: ctyp * ctyp -> bool
   val aconvc: cterm * cterm -> bool
-  val add_tvars: thm -> ctyp list -> ctyp list
-  val add_frees: thm -> cterm list -> cterm list
-  val add_vars: thm -> cterm list -> cterm list
+  val add_tvars: thm -> ctyp Term_Subst.TVars.table -> ctyp Term_Subst.TVars.table
+  val add_vars: thm -> cterm Term_Subst.Vars.table -> cterm Term_Subst.Vars.table
   val dest_funT: ctyp -> ctyp * ctyp
   val strip_type: ctyp -> ctyp list * ctyp
   val all_name: Proof.context -> string * cterm -> cterm -> cterm
@@ -76,6 +75,7 @@
   val instantiate_frees: ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> thm -> thm
   val instantiate': ctyp option list -> cterm option list -> thm -> thm
   val forall_intr_frees: thm -> thm
+  val forall_intr_vars: thm -> thm
   val unvarify_global: theory -> thm -> thm
   val unvarify_axiom: theory -> string -> thm
   val rename_params_rule: string list * int -> thm -> thm
@@ -137,9 +137,15 @@
 val eq_ctyp = op = o apply2 Thm.typ_of;
 val op aconvc = op aconv o apply2 Thm.term_of;
 
-val add_tvars = Thm.fold_atomic_ctyps (fn a => is_TVar (Thm.typ_of a) ? insert eq_ctyp a);
-val add_frees = Thm.fold_atomic_cterms (fn a => is_Free (Thm.term_of a) ? insert (op aconvc) a);
-val add_vars = Thm.fold_atomic_cterms (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a);
+val add_tvars =
+  Thm.fold_atomic_ctyps {hyps = false} Term.is_TVar (fn cT => fn tab =>
+    let val v = Term.dest_TVar (Thm.typ_of cT)
+    in tab |> not (Term_Subst.TVars.defined tab v) ? Term_Subst.TVars.update (v, cT) end);
+
+val add_vars =
+  Thm.fold_atomic_cterms {hyps = false} Term.is_Var (fn ct => fn tab =>
+    let val v = Term.dest_Var (Thm.term_of ct)
+    in tab |> not (Term_Subst.Vars.defined tab v) ? Term_Subst.Vars.update (v, ct) end);
 
 
 (* ctyp operations *)
@@ -378,7 +384,7 @@
 fun forall_elim_vars_list vars i th =
   let
     val used =
-      (Thm.fold_terms o Term.fold_aterms)
+      (Thm.fold_terms {hyps = false} o Term.fold_aterms)
         (fn Var ((x, j), _) => if i = j then insert (op =) x else I | _ => I) th [];
     val vars' = (Name.variant_list used (map #1 vars), vars)
       |> ListPair.map (fn (x, (_, T)) => Thm.var ((x, i), T));
@@ -408,8 +414,8 @@
         val idx = Thm.maxidx_of th + 1;
         fun index ((a, A), b) = (((a, idx), A), b);
         val insts = (map index instT, map index inst);
-        val tfrees = fold (Symtab.insert_set o #1 o #1) instT Symtab.empty;
-        val frees = fold (Symtab.insert_set o #1 o #1) inst Symtab.empty;
+        val tfrees = Symtab.build (fold (Symtab.insert_set o #1 o #1) instT);
+        val frees = Symtab.build (fold (Symtab.insert_set o #1 o #1) inst);
 
         val hyps = Thm.chyps_of th;
         val inst_cterm =
@@ -437,24 +443,40 @@
       zip_options xs ys handle ListPair.UnequalLengths =>
         err "more instantiations than variables in thm";
 
-    val thm' =
-      Thm.instantiate ((zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm;
-    val thm'' =
-      Thm.instantiate ([], zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts) thm';
-  in thm'' end;
+    val instT = zip_vars (build_rev (Thm.fold_terms {hyps = false} Term.add_tvars thm)) cTs;
+    val thm' = Thm.instantiate (instT, []) thm;
+    val inst = zip_vars (build_rev (Thm.fold_terms {hyps = false} Term.add_vars thm')) cts;
+  in Thm.instantiate ([], inst) thm' end;
 
 
-(* forall_intr_frees: generalization over all suitable Free variables *)
+(* implicit generalization over variables -- canonical order *)
+
+fun forall_intr_vars th =
+  let
+    val (_, vars) =
+      (th, (Term_Subst.Vars.empty, [])) |-> Thm.fold_atomic_cterms {hyps = false} Term.is_Var
+        (fn ct => fn (seen, vars) =>
+          let val v = Term.dest_Var (Thm.term_of ct) in
+            if not (Term_Subst.Vars.defined seen v)
+            then (Term_Subst.Vars.add (v, ()) seen, ct :: vars)
+            else (seen, vars)
+          end);
+  in fold Thm.forall_intr vars th end;
 
 fun forall_intr_frees th =
   let
     val fixed =
-      fold Term.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th) @ 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
-        | _ => I)) th [];
+      Term_Subst.Frees.build
+       (fold Term_Subst.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th)) #>
+        fold Term_Subst.add_frees (Thm.hyps_of th));
+    val (_, frees) =
+      (th, (fixed, [])) |-> Thm.fold_atomic_cterms {hyps = false} Term.is_Free
+        (fn ct => fn (seen, frees) =>
+          let val v = Term.dest_Free (Thm.term_of ct) in
+            if not (Term_Subst.Frees.defined seen v)
+            then (Term_Subst.Frees.add (v, ()) seen, ct :: frees)
+            else (seen, frees)
+          end);
   in fold Thm.forall_intr frees th end;
 
 
@@ -466,12 +488,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 =
+      Term_Subst.TVars.build (prop |> (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 =
+      Term_Subst.Vars.build (prop |> 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;
 
@@ -515,7 +552,7 @@
 
 fun stripped_sorts thy t =
   let
-    val tfrees = rev (Term.add_tfrees t []);
+    val tfrees = build_rev (Term.add_tfrees t);
     val tfrees' = map (fn a => (a, [])) (Name.variant_list [] (map #1 tfrees));
     val recover =
       map2 (fn (a', S') => fn (a, S) => (((a', 0), S'), Thm.global_ctyp_of thy (TVar ((a, 0), S))))
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/morphism.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -138,11 +138,11 @@
   | instantiate_frees_morphism (cinstT, cinst) =
       let
         val instT =
-          fold (fn (v, cT) => Term_Subst.TFrees.add (v, Thm.typ_of cT))
-            cinstT Term_Subst.TFrees.empty;
+          Term_Subst.TFrees.build
+            (cinstT |> fold (fn (v, cT) => Term_Subst.TFrees.add (v, Thm.typ_of cT)));
         val inst =
-          fold (fn (v, ct) => Term_Subst.Frees.add (v, Thm.term_of ct))
-            cinst Term_Subst.Frees.empty;
+          Term_Subst.Frees.build
+            (cinst |> fold (fn (v, ct) => Term_Subst.Frees.add (v, Thm.term_of ct)));
       in
         morphism "instantiate_frees"
           {binding = [],
@@ -157,11 +157,11 @@
   | instantiate_morphism (cinstT, cinst) =
       let
         val instT =
-          fold (fn (v, cT) => Term_Subst.TVars.add (v, Thm.typ_of cT))
-            cinstT Term_Subst.TVars.empty;
+          Term_Subst.TVars.build (cinstT |> fold (fn (v, cT) =>
+            Term_Subst.TVars.add (v, Thm.typ_of cT)));
         val inst =
-          fold (fn (v, ct) => Term_Subst.Vars.add (v, Thm.term_of ct))
-            cinst Term_Subst.Vars.empty;
+          Term_Subst.Vars.build (cinst |> fold (fn (v, ct) =>
+            Term_Subst.Vars.add (v, Thm.term_of ct)));
       in
         morphism "instantiate"
           {binding = [],
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/primitive_defs.ML
--- a/src/Pure/primitive_defs.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/primitive_defs.ML	Tue Sep 07 10:17:03 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.TFrees.build (Term_Subst.add_tfrees head);
 
     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
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/proofterm.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -109,7 +109,7 @@
   val implies_intr_proof': term -> proof -> proof
   val forall_intr_proof: string * term -> typ option -> proof -> proof
   val forall_intr_proof': term -> proof -> proof
-  val varify_proof: term -> (string * sort) list -> proof -> proof
+  val varify_proof: term -> Term_Subst.TFrees.set -> proof -> proof
   val legacy_freezeT: term -> proof -> proof
   val rotate_proof: term list -> term -> (string * typ) list -> term list -> int -> proof -> proof
   val permute_prems_proof: term list -> int -> int -> proof -> proof
@@ -671,25 +671,37 @@
 
 (* substitutions *)
 
-fun del_conflicting_tvars envT T =
+local
+
+fun conflicting_tvarsT envT =
+  Term.fold_atyps
+    (fn T => fn instT =>
+      (case T of
+        TVar (v as (_, S)) =>
+          if Term_Subst.TVars.defined instT v orelse can (Type.lookup envT) v then instT
+          else Term_Subst.TVars.update (v, Logic.dummy_tfree S) instT
+      | _ => instT));
+
+fun conflicting_tvars env =
+  Term.fold_aterms
+    (fn t => fn inst =>
+      (case t of
+        Var (v as (_, T)) =>
+          if Term_Subst.Vars.defined inst v orelse can (Envir.lookup env) v then inst
+          else Term_Subst.Vars.update (v, Free ("dummy", T)) inst
+      | _ => inst));
+
+fun del_conflicting_tvars envT ty =
+  Term_Subst.instantiateT (Term_Subst.TVars.build (conflicting_tvarsT envT ty)) ty;
+
+fun del_conflicting_vars env tm =
   let
     val instT =
-      map_filter (fn ixnS as (_, S) =>
-        (Type.lookup envT ixnS; NONE) handle TYPE _ =>
-          SOME (ixnS, Logic.dummy_tfree S)) (Term.add_tvarsT T [])
-  in Term_Subst.instantiateT (Term_Subst.TVars.table instT) T end;
+      Term_Subst.TVars.build (tm |> Term.fold_types (conflicting_tvarsT (Envir.type_env env)));
+    val inst = Term_Subst.Vars.build (tm |> conflicting_tvars env);
+  in Term_Subst.instantiate (instT, inst) tm end;
 
-fun del_conflicting_vars env t =
-  let
-    val instT =
-      map_filter (fn ixnS as (_, S) =>
-        (Type.lookup (Envir.type_env env) ixnS; NONE) handle TYPE _ =>
-          SOME (ixnS, Logic.dummy_tfree S)) (Term.add_tvars t []);
-    val inst =
-      map_filter (fn (ixnT as (_, T)) =>
-        (Envir.lookup env ixnT; NONE) handle TYPE _ =>
-          SOME (ixnT, Free ("dummy", T))) (Term.add_vars t []);
-  in Term_Subst.instantiate (Term_Subst.TVars.make instT, Term_Subst.Vars.table inst) t end;
+in
 
 fun norm_proof env =
   let
@@ -726,6 +738,8 @@
       | norm _ = raise Same.SAME;
   in Same.commit norm end;
 
+end;
+
 
 (* remove some types in proof term (to save space) *)
 
@@ -887,8 +901,9 @@
 
 fun varify_proof t fixed prf =
   let
-    val fs = Term.fold_types (Term.fold_atyps
-      (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
+    val fs =
+      build (t |> (Term.fold_types o Term.fold_atyps)
+        (fn TFree v => if Term_Subst.TFrees.defined fixed v then I else insert (op =) v | _ => I));
     val used = Name.context
       |> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
     val fmap = fs ~~ #1 (fold_map Name.variant (map fst fs) used);
@@ -1110,7 +1125,7 @@
   | is_fun (TVar _) = true
   | is_fun _ = false;
 
-fun vars_of t = map Var (rev (Term.add_vars t []));
+fun vars_of t = map Var (build_rev (Term.add_vars t));
 
 fun add_funvars Ts (vs, t) =
   if is_fun (fastype_of1 (Ts, t)) then
@@ -2131,7 +2146,7 @@
 
     fun export_body (PBody {thms, ...}) = fold export_thm thms;
 
-    val exports = (bodies, Inttab.empty) |-> fold export_body |> Inttab.dest;
+    val exports = Inttab.build (fold export_body bodies) |> Inttab.dest;
   in List.app (Lazy.force o #2) exports end;
 
 local
@@ -2312,7 +2327,7 @@
             end)
       | boxes_of MinProof = raise MIN_PROOF ()
       | boxes_of _ = I;
-  in Inttab.fold_rev (cons o #2) (fold boxes_of proofs Inttab.empty) [] end;
+  in Inttab.fold_rev (cons o #2) (Inttab.build (fold boxes_of proofs)) [] end;
 
 end;
 
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/raw_simplifier.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -161,13 +161,13 @@
 fun rewrite_rule_extra_vars prems elhs erhs =
   let
     val elhss = elhs :: prems;
-    val tvars = fold Term.add_tvars elhss [];
-    val vars = fold Term.add_vars elhss [];
+    val tvars = Term_Subst.TVars.build (fold Term_Subst.add_tvars elhss);
+    val vars = Term_Subst.Vars.build (fold Term_Subst.add_vars elhss);
   in
     erhs |> Term.exists_type (Term.exists_subtype
-      (fn TVar v => not (member (op =) tvars v) | _ => false)) orelse
+      (fn TVar v => not (Term_Subst.TVars.defined tvars v) | _ => false)) orelse
     erhs |> Term.exists_subterm
-      (fn Var v => not (member (op =) vars v) | _ => false)
+      (fn Var v => not (Term_Subst.Vars.defined vars v) | _ => false)
   end;
 
 fun rrule_extra_vars elhs thm =
@@ -474,6 +474,8 @@
     (cond_warning ctxt (fn () => print_thm ctxt "Ignoring duplicate rewrite rule:" ("", thm));
       ctxt));
 
+val vars_set = Term_Subst.Vars.build o Term_Subst.add_vars;
+
 local
 
 fun vperm (Var _, Var _) = true
@@ -481,8 +483,7 @@
   | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
   | vperm (t, u) = (t = u);
 
-fun var_perm (t, u) =
-  vperm (t, u) andalso eq_set (op =) (Term.add_vars t [], Term.add_vars u []);
+fun var_perm (t, u) = vperm (t, u) andalso Term_Subst.Vars.eq_set (apply2 vars_set (t, u));
 
 in
 
@@ -945,7 +946,7 @@
   while the premises are solved.*)
 
 fun cond_skel (args as (_, (lhs, rhs))) =
-  if subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args
+  if Term_Subst.Vars.subset (vars_set rhs, vars_set lhs) then uncond_skel args
   else skel0;
 
 (*
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/sorts.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -257,9 +257,8 @@
 
 (* classrel *)
 
-fun rebuild_arities context algebra = algebra |> map_arities (fn arities =>
-  Symtab.empty
-  |> add_arities_table context algebra arities);
+fun rebuild_arities context algebra = algebra
+  |> map_arities (Symtab.build o add_arities_table context algebra);
 
 fun add_classrel context rel = rebuild_arities context o map_classes (fn classes =>
   classes |> Graph.add_edge_trans_acyclic rel
@@ -286,12 +285,11 @@
             if pointer_eq (ars1, ars2) then raise Symtab.SAME
             else insert_ars context algebra0 t ars2 ars1)
       | (false, true) =>  (*unary completion*)
-          Symtab.empty
-          |> add_arities_table context algebra0 arities1
+          Symtab.build (add_arities_table context algebra0 arities1)
       | (false, false) => (*binary completion*)
-          Symtab.empty
-          |> add_arities_table context algebra0 arities1
-          |> add_arities_table context algebra0 arities2);
+          Symtab.build
+           (add_arities_table context algebra0 arities1 #>
+            add_arities_table context algebra0 arities2));
   in make_algebra (classes', arities') end;
 
 
@@ -301,16 +299,16 @@
   let
     fun new_classrel rel = not (exists (fn algebra => class_less algebra rel) parents);
     val classrel =
-      (classes, []) |-> Graph.fold (fn (c, (_, (_, ds))) =>
+      build (classes |> Graph.fold (fn (c, (_, (_, ds))) =>
         (case filter (fn d => new_classrel (c, d)) (Graph.Keys.dest ds) of
           [] => I
-        | ds' => cons (c, sort_strings ds')))
+        | ds' => cons (c, sort_strings ds'))))
       |> sort_by #1;
 
     fun is_arity t ar algebra = member (op =) (Symtab.lookup_list (arities_of algebra) t) ar;
     fun add_arity t (c, Ss) = not (exists (is_arity t (c, Ss)) parents) ? cons (t, Ss, c);
     val arities =
-      (arities, []) |-> Symtab.fold (fn (t, ars) => fold_rev (add_arity t) (sort_by #1 ars))
+      build (arities |> Symtab.fold (fn (t, ars) => fold_rev (add_arity t) (sort_by #1 ars)))
       |> sort_by #1;
   in {classrel = classrel, arities = arities} end;
 
@@ -390,7 +388,7 @@
   in uncurry meet end;
 
 fun meet_sort_typ algebra (T, S) =
-  let val tab = meet_sort algebra (T, S) Vartab.empty;
+  let val tab = Vartab.build (meet_sort algebra (T, S));
   in Term.map_type_tvar (fn (v, _) => TVar (v, (the o Vartab.lookup tab) v)) end;
 
 
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/term_subst.ML
--- a/src/Pure/term_subst.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/term_subst.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -17,7 +17,7 @@
 structure Tab = Table(Key);
 
 fun add entry = Tab.insert (K true) entry;
-fun table entries = fold add entries Tab.empty;
+fun table entries = Tab.build (fold add entries);
 
 open Tab;
 
@@ -29,6 +29,15 @@
   structure TVars: INST_TABLE
   structure Frees: INST_TABLE
   structure Vars: INST_TABLE
+  val add_tfreesT: typ -> TFrees.set -> TFrees.set
+  val add_tfrees: term -> TFrees.set -> TFrees.set
+  val add_tvarsT: typ -> TVars.set -> TVars.set
+  val add_tvars: term -> TVars.set -> TVars.set
+  val add_frees: term -> Frees.set -> Frees.set
+  val add_vars: term -> Vars.set -> Vars.set
+  val add_tfree_namesT: typ -> Symtab.set -> Symtab.set
+  val add_tfree_names: term -> Symtab.set -> Symtab.set
+  val add_free_names: term -> Symtab.set -> Symtab.set
   val map_atypsT_same: typ Same.operation -> typ Same.operation
   val map_types_same: typ Same.operation -> term Same.operation
   val map_aterms_same: term Same.operation -> term Same.operation
@@ -77,6 +86,16 @@
   val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.typ_ord)
 );
 
+val add_tfreesT = fold_atyps (fn TFree v => TFrees.add (v, ()) | _ => I);
+val add_tfrees = fold_types add_tfreesT;
+val add_tvarsT = fold_atyps (fn TVar v => TVars.add (v, ()) | _ => I);
+val add_tvars = fold_types add_tvarsT;
+val add_frees = fold_aterms (fn Free v => Frees.add (v, ()) | _ => I);
+val add_vars = fold_aterms (fn Var v => Vars.add (v, ()) | _ => I);
+val add_tfree_namesT = fold_atyps (fn TFree (a, _) => Symtab.insert_set a | _ => I);
+val add_tfree_names = fold_types add_tfree_namesT;
+val add_free_names = fold_aterms (fn Free (x, _) => Symtab.insert_set x | _ => I);
+
 
 (* generic mapping *)
 
@@ -256,12 +275,12 @@
   let
     val (instT, _) =
       (TVars.empty, used) |> TVars.fold (zero_var_inst TVars.add TVar o #1)
-        ((fold o fold_types o fold_atyps) (fn TVar v =>
-          TVars.add (v, ()) | _ => I) ts TVars.empty);
+        (TVars.build (ts |> (fold o fold_types o fold_atyps)
+          (fn TVar v => TVars.add (v, ()) | _ => I)));
     val (inst, _) =
       (Vars.empty, used) |> Vars.fold (zero_var_inst Vars.add Var o #1)
-        ((fold o fold_aterms) (fn Var (xi, T) =>
-          Vars.add ((xi, instantiateT instT T), ()) | _ => I) ts Vars.empty);
+        (Vars.build (ts |> (fold o fold_aterms)
+          (fn Var (xi, T) => Vars.add ((xi, instantiateT instT T), ()) | _ => I)));
   in (instT, inst) end;
 
 fun zero_var_indexes_list ts = map (instantiate (zero_var_indexes_inst Name.context ts)) ts;
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/theory.ML	Tue Sep 07 10:17:03 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 = Term_Subst.TFrees.build (snd lhs |> fold Term_Subst.add_tfreesT);
     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 [];
+      build (rhs |> fold (#2 #> (fold o Term.fold_atyps)
+        (fn TFree v => not (Term_Subst.TFrees.defined lhs_vars v) ? insert (op =) v | _ => I)));
     val _ =
       if null rhs_extras then ()
       else error ("Specification depends on extra type variables: " ^
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/thm.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -59,9 +59,9 @@
   val first_order_match: cterm * cterm ->
     ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
   (*theorems*)
-  val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
-  val fold_atomic_ctyps: (ctyp -> 'a -> 'a) -> thm -> 'a -> 'a
-  val fold_atomic_cterms: (cterm -> 'a -> 'a) -> thm -> 'a -> 'a
+  val fold_terms: {hyps: bool} -> (term -> 'a -> 'a) -> thm -> 'a -> 'a
+  val fold_atomic_ctyps: {hyps: bool} -> (typ -> bool) -> (ctyp -> 'a -> 'a) -> thm -> 'a -> 'a
+  val fold_atomic_cterms: {hyps: bool} -> (term -> bool) -> (cterm -> 'a -> 'a) -> thm -> 'a -> 'a
   val terms_of_tpairs: (term * term) list -> term list
   val full_prop_of: thm -> term
   val theory_id: thm -> Context.theory_id
@@ -161,7 +161,7 @@
   val trivial: cterm -> thm
   val of_class: ctyp * class -> thm
   val unconstrainT: thm -> thm
-  val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
+  val varifyT_global': Term_Subst.TFrees.set -> thm -> ((string * sort) * indexname) list * thm
   val varifyT_global: thm -> thm
   val legacy_freezeT: thm -> thm
   val plain_prop_of: thm -> term
@@ -434,19 +434,22 @@
 
 fun rep_thm (Thm (_, args)) = args;
 
-fun fold_terms f (Thm (_, {tpairs, prop, hyps, ...})) =
-  fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps;
+fun fold_terms h f (Thm (_, {tpairs, prop, hyps, ...})) =
+  fold (fn (t, u) => f t #> f u) tpairs #> f prop #> #hyps h ? fold f hyps;
 
-fun fold_atomic_ctyps f (th as Thm (_, {cert, maxidx, shyps, ...})) =
+fun fold_atomic_ctyps h g f (th as Thm (_, {cert, maxidx, shyps, ...})) =
   let fun ctyp T = Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = shyps}
-  in (fold_terms o fold_types o fold_atyps) (f o ctyp) th end;
+  in (fold_terms h o fold_types o fold_atyps) (fn T => if g T then f (ctyp T) else I) th end;
 
-fun fold_atomic_cterms f (th as Thm (_, {cert, maxidx, shyps, ...})) =
-  let fun cterm t T = Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = shyps} in
-    (fold_terms o fold_aterms)
-      (fn t as Const (_, T) => f (cterm t T)
-        | t as Free (_, T) => f (cterm t T)
-        | t as Var (_, T) => f (cterm t T)
+fun fold_atomic_cterms h g f (th as Thm (_, {cert, maxidx, shyps, ...})) =
+  let
+    fun cterm t T = Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = shyps};
+    fun apply t T = if g t then f (cterm t T) else I;
+  in
+    (fold_terms h o fold_aterms)
+      (fn t as Const (_, T) => apply t T
+        | t as Free (_, T) => apply t T
+        | t as Var (_, T) => apply t T
         | _ => I) th
   end;
 
@@ -985,7 +988,7 @@
 
 (*Dangling sort constraints of a thm*)
 fun extra_shyps (th as Thm (_, {shyps, ...})) =
-  Sorts.subtract (fold_terms Sorts.insert_term th []) shyps;
+  Sorts.subtract (fold_terms {hyps = true} Sorts.insert_term th []) shyps;
 
 (*Remove extra sorts that are witnessed by type signature information*)
 fun strip_shyps thm =
@@ -1001,7 +1004,8 @@
         fun lt (S1, S2) = le (S1, S2) andalso not (le (S2, S1));
         fun rel (S1, S2) = if S1 = S2 then [] else [(Term.aT S1, S2)];
 
-        val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm [];
+        val present =
+          (fold_terms {hyps = true} o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm [];
         val extra = fold (Sorts.remove_sort o #2) present shyps;
         val witnessed = Sign.witness_sorts thy present extra;
         val non_witnessed = fold (Sorts.remove_sort o #2) witnessed extra |> map (`minimize);
@@ -1641,8 +1645,8 @@
       |> fold add_instT_sorts instT
       |> fold add_inst_sorts inst;
 
-    val instT' = fold (add_instT thy') instT Term_Subst.TVars.empty;
-    val inst' = fold (add_inst thy') inst Term_Subst.Vars.empty;
+    val instT' = Term_Subst.TVars.build (fold (add_instT thy') instT);
+    val inst' = Term_Subst.Vars.build (fold (add_inst thy') inst);
   in ((instT', inst'), (cert', sorts')) end;
 
 in
@@ -1752,7 +1756,7 @@
       fun err msg = raise THM ("unconstrainT: " ^ msg, 0, [thm]);
       val _ = null hyps orelse err "bad hyps";
       val _ = null tpairs orelse err "bad flex-flex constraints";
-      val tfrees = rev (Term.add_tfree_names prop []);
+      val tfrees = build_rev (Term.add_tfree_names prop);
       val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees);
 
       val ps = map (apsnd (Future.map fulfill_body)) promises;
@@ -1776,7 +1780,7 @@
 (*Replace all TFrees not fixed or in the hyps by new TVars*)
 fun varifyT_global' fixed (Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) =
   let
-    val tfrees = fold Term.add_tfrees hyps fixed;
+    val tfrees = fold Term_Subst.add_tfrees hyps fixed;
     val prop1 = attach_tpairs tpairs prop;
     val (al, prop2) = Type.varify_global tfrees prop1;
     val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
@@ -1792,7 +1796,7 @@
       prop = prop3}))
   end;
 
-val varifyT_global = #2 o varifyT_global' [];
+val varifyT_global = #2 o varifyT_global' Term_Subst.TFrees.empty;
 
 (*Replace all TVars by TFrees that are often new*)
 fun legacy_freezeT (Thm (der, {cert, constraints, shyps, hyps, tpairs, prop, ...})) =
@@ -2093,7 +2097,7 @@
     val add_vars =
       full_prop_of #>
       fold_aterms (fn Var v => Vartab.insert_list (op =) v | _ => I);
-    val vars = Vartab.empty |> add_vars th1 |> add_vars th2;
+    val vars = Vartab.build (add_vars th1 #> add_vars th2);
   in SOME (Vartab.fold (unify_vars o #2) vars env) end
   handle Pattern.Unif => NONE;
 
@@ -2257,7 +2261,7 @@
 fun standard_tvars thm =
   let
     val thy = theory_of_thm thm;
-    val tvars = rev (Term.add_tvars (prop_of thm) []);
+    val tvars = build_rev (Term.add_tvars (prop_of thm));
     val names = Name.invent Name.context Name.aT (length tvars);
     val tinst =
       map2 (fn (ai, S) => fn b => ((ai, S), global_ctyp_of thy (TVar ((b, 0), S)))) tvars names;
@@ -2300,8 +2304,8 @@
 (* type arities *)
 
 fun thynames_of_arity thy (a, c) =
-  (get_arities thy, []) |-> Aritytab.fold
-    (fn ((a', _, c'), (_, name, ser)) => (a = a' andalso c = c') ? cons (name, ser))
+  build (get_arities thy |> Aritytab.fold
+    (fn ((a', _, c'), (_, name, ser)) => (a = a' andalso c = c') ? cons (name, ser)))
   |> sort (int_ord o apply2 #2) |> map #1;
 
 fun insert_arity_completions thy ((t, Ss, c), (th, thy_name, ser)) (finished, arities) =
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/thm_deps.ML
--- a/src/Pure/thm_deps.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/thm_deps.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -67,7 +67,7 @@
         end;
   in
     fn thms =>
-      (fold (fold deps o Thm.thm_deps o Thm.transfer thy) thms Inttab.empty, [])
+      (Inttab.build (fold (fold deps o Thm.thm_deps o Thm.transfer thy) thms), [])
       |-> Inttab.fold_rev (fn (_, SOME entry) => cons entry | _ => I)
   end;
 
@@ -119,12 +119,13 @@
     fun is_unused a = not (Symtab.defined used a);
 
     (*groups containing at least one used theorem*)
-    val used_groups = fold (fn (a, (_, _, group)) =>
-      if is_unused a then I
-      else
-        (case group of
-          NONE => I
-        | SOME grp => Inttab.update (grp, ()))) new_thms Inttab.empty;
+    val used_groups =
+      Inttab.build (new_thms |> fold (fn (a, (_, _, group)) =>
+        if is_unused a then I
+        else
+          (case group of
+            NONE => I
+          | SOME grp => Inttab.update (grp, ()))));
 
     val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) =>
       if not concealed andalso
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/type.ML
--- a/src/Pure/type.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/type.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -61,7 +61,7 @@
   val strip_sorts: typ -> typ
   val strip_sorts_dummy: typ -> typ
   val no_tvars: typ -> typ
-  val varify_global: (string * sort) list -> term -> ((string * sort) * indexname) list * term
+  val varify_global: Term_Subst.TFrees.set -> term -> ((string * sort) * indexname) list * term
   val legacy_freeze_thaw_type: typ -> typ * (typ -> typ)
   val legacy_freeze_type: typ -> typ
   val legacy_freeze_thaw: term -> term * (term -> term)
@@ -355,8 +355,9 @@
 
 fun varify_global fixed t =
   let
-    val fs = Term.fold_types (Term.fold_atyps
-      (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
+    val fs =
+      build (t |> (Term.fold_types o Term.fold_atyps)
+        (fn TFree v => if Term_Subst.TFrees.defined fixed v then I else insert (op =) v | _ => I));
     val used = Name.context
       |> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
     val fmap = fs ~~ map (rpair 0) (#1 (fold_map Name.variant (map fst fs) used));
@@ -446,7 +447,7 @@
   in match end;
 
 fun typ_instance tsig (T, U) =
-  (typ_match tsig (U, T) Vartab.empty; true) handle TYPE_MATCH => false;
+  (Vartab.build (typ_match tsig (U, T)); true) handle TYPE_MATCH => false;
 
 (*purely structural matching*)
 fun raw_match (TVar (v, S), T) subs =
@@ -474,7 +475,7 @@
 
 fun raw_instance (T, U) =
   if could_match (U, T) then
-    (raw_match (U, T) Vartab.empty; true) handle TYPE_MATCH => false
+    (Vartab.build (raw_match (U, T)); true) handle TYPE_MATCH => false
   else false;
 
 
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Pure/variable.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -74,11 +74,10 @@
     (typ Term_Subst.TVars.table * term Term_Subst.Vars.table) * Proof.context
   val importT_terms: term list -> Proof.context -> term list * Proof.context
   val import_terms: bool -> term list -> Proof.context -> term list * Proof.context
-  val importT: thm list -> Proof.context ->
-    (((indexname * sort) * ctyp) list * thm list) * Proof.context
+  val importT: thm list -> Proof.context -> (ctyp Term_Subst.TVars.table * thm list) * Proof.context
   val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context
   val import: bool -> thm list -> Proof.context ->
-    ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context
+    ((ctyp Term_Subst.TVars.table * cterm Term_Subst.Vars.table) * thm list) * Proof.context
   val import_vars: Proof.context -> thm -> thm
   val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
   val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
@@ -268,7 +267,7 @@
 val declare_prf =
   Proofterm.fold_proof_terms_types declare_internal (declare_internal o Logic.mk_type);
 
-val declare_thm = Thm.fold_terms declare_internal;
+val declare_thm = Thm.fold_terms {hyps = true} declare_internal;
 
 
 (* renaming term/type frees *)
@@ -516,14 +515,14 @@
     val still_fixed = not o is_newly_fixed inner outer;
 
     val gen_fixes =
-      Name_Space.fold_table (fn (y, _) => not (is_fixed outer y) ? Symtab.insert_set y)
-        (fixes_of inner) Symtab.empty;
+      Symtab.build (fixes_of inner |> Name_Space.fold_table (fn (y, _) =>
+        not (is_fixed outer y) ? Symtab.insert_set y));
 
     val type_occs_inner = type_occs_of inner;
     fun gen_fixesT ts =
-      Symtab.fold (fn (a, xs) =>
+      Symtab.build (fold decl_type_occs ts type_occs_inner |> Symtab.fold (fn (a, xs) =>
         if declared_outer a orelse exists still_fixed xs
-        then I else Symtab.insert_set a) (fold decl_type_occs ts type_occs_inner) Symtab.empty;
+        then I else Symtab.insert_set a));
   in (gen_fixesT, gen_fixes) end;
 
 fun exportT_inst inner outer = #1 (export_inst inner outer);
@@ -591,22 +590,22 @@
 
 fun importT_inst ts ctxt =
   let
-    val tvars = rev (fold Term.add_tvars ts []);
+    val tvars = build_rev (fold Term.add_tvars ts);
     val (tfrees, ctxt') = invent_types (map #2 tvars) ctxt;
     val instT =
-      fold2 (fn a => fn b => Term_Subst.TVars.add (a, TFree b))
-        tvars tfrees Term_Subst.TVars.empty;
+      Term_Subst.TVars.build (fold2 (fn a => fn b =>
+        Term_Subst.TVars.add (a, TFree b)) tvars tfrees);
   in (instT, ctxt') end;
 
 fun import_inst is_open ts ctxt =
   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)) (rev (fold Term.add_vars ts []));
+    val vars = map (apsnd (Term_Subst.instantiateT instT)) (build_rev (fold Term.add_vars ts));
     val (ys, ctxt'') = variant_fixes (map (ren o #1 o #1) vars) ctxt';
     val inst =
-      fold2 (fn (x, T) => fn y => Term_Subst.Vars.add ((x, T), Free (y, T)))
-        vars ys Term_Subst.Vars.empty;
+      Term_Subst.Vars.build (fold2 (fn (x, T) => fn y =>
+        Term_Subst.Vars.add ((x, T), Free (y, T))) vars ys);
   in ((instT, inst), ctxt'') end;
 
 fun importT_terms ts ctxt =
@@ -620,8 +619,8 @@
 fun importT ths ctxt =
   let
     val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
-    val instT' = Term_Subst.TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt' T)) instT [];
-    val ths' = map (Thm.instantiate (instT', [])) ths;
+    val instT' = Term_Subst.TVars.map (K (Thm.ctyp_of ctxt')) instT;
+    val ths' = map (Thm.instantiate (Term_Subst.TVars.dest instT', [])) ths;
   in ((instT', ths'), ctxt') end;
 
 fun import_prf is_open prf ctxt =
@@ -633,9 +632,9 @@
 fun import is_open ths ctxt =
   let
     val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
-    val instT' = Term_Subst.TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt' T)) instT [];
-    val inst' = Term_Subst.Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt' t)) inst [];
-    val ths' = map (Thm.instantiate (instT', inst')) ths;
+    val instT' = Term_Subst.TVars.map (K (Thm.ctyp_of ctxt')) instT;
+    val inst' = Term_Subst.Vars.map (K (Thm.cterm_of ctxt')) inst;
+    val ths' = map (Thm.instantiate (Term_Subst.TVars.dest instT', Term_Subst.Vars.dest inst')) ths;
   in (((instT', inst'), ths'), ctxt') end;
 
 fun import_vars ctxt th =
@@ -691,10 +690,10 @@
 
 fun focus_subgoal bindings i st =
   let
-    val all_vars = Thm.fold_terms Term.add_vars st [];
+    val all_vars = Term_Subst.Vars.build (Thm.fold_terms {hyps = false} Term_Subst.add_vars st);
   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;
 
@@ -733,8 +732,8 @@
     val occs = type_occs_of ctxt;
     val occs' = type_occs_of ctxt';
     val types =
-      Symtab.fold (fn (a, _) =>
-        if Symtab.defined occs a then I else Symtab.insert_set a) occs' Symtab.empty;
+      Symtab.build (occs' |> Symtab.fold (fn (a, _) =>
+        if Symtab.defined occs a then I else Symtab.insert_set a));
     val idx = maxidx_of ctxt' + 1;
     val Ts' = (fold o fold_types o fold_atyps)
       (fn T as TFree _ =>
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Tools/Code/code_printer.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -142,10 +142,9 @@
 fun markup_stmt sym = with_presentation_marker
   (Pretty.mark (code_presentationN, [(stmt_nameN, Code_Symbol.marker sym)]));
 
-fun filter_presentation [] tree =
-      Buffer.empty
-      |> fold XML.add_content tree
-  | filter_presentation presentation_syms tree =
+fun filter_presentation [] xml =
+      Buffer.build (fold XML.add_content xml)
+  | filter_presentation presentation_syms xml =
       let
         val presentation_idents = map Code_Symbol.marker presentation_syms
         fun is_selected (name, attrs) =
@@ -159,7 +158,7 @@
         fun filter (XML.Elem (name_attrs, xs)) =
               fold (if is_selected name_attrs then add_content_with_space else filter) xs
           | filter (XML.Text _) = I;
-      in snd (fold filter tree (true, Buffer.empty)) end;
+      in snd (fold filter xml (true, Buffer.empty)) end;
 
 fun format presentation_names width =
   with_presentation_marker (Pretty.string_of_margin width)
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Tue Sep 07 10:17:03 2021 +0200
@@ -572,11 +572,12 @@
 See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/buffer.ML\<close>.
 -}
 
-module Isabelle.Buffer (T, empty, add, content)
+module Isabelle.Buffer (T, empty, add, content, build, build_content)
 where
 
 import qualified Isabelle.Bytes as Bytes
 import Isabelle.Bytes (Bytes)
+import Isabelle.Library
 
 
 newtype T = Buffer [Bytes]
@@ -589,6 +590,12 @@
 
 content :: T -> Bytes
 content (Buffer bs) = Bytes.concat (reverse bs)
+
+build :: (T -> T) -> T
+build f = f empty
+
+build_content :: (T -> T) -> Bytes
+build_content f = build f |> content
 \<close>
 
 generate_file "Isabelle/Value.hs" = \<open>
@@ -1522,7 +1529,7 @@
         Text s -> Buffer.add s
 
 content_of :: Body -> Bytes
-content_of body = Buffer.empty |> fold add_content body |> Buffer.content
+content_of = Buffer.build_content . fold add_content
 
 
 {- string representation -}
@@ -1540,7 +1547,7 @@
 
 instance Show Tree where
   show tree =
-    Buffer.empty |> show_tree tree |> Buffer.content |> make_string
+    make_string $ Buffer.build_content (show_tree tree)
     where
       show_tree (Elem ((name, atts), [])) =
         Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>"
@@ -1831,7 +1838,7 @@
 buffer (XML.Text s) = Buffer.add s
 
 string_of_body :: XML.Body -> Bytes
-string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content
+string_of_body = Buffer.build_content . buffer_body
 
 string_of :: XML.Tree -> Bytes
 string_of = string_of_body . single
@@ -2049,7 +2056,7 @@
 formatted = YXML.string_of_body . symbolic
 
 unformatted :: T -> Bytes
-unformatted prt = Buffer.empty |> out prt |> Buffer.content
+unformatted = Buffer.build_content . out
   where
     out (Block markup _ _ prts) =
       let (bg, en) = YXML.output_markup markup
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Tools/IsaPlanner/rw_inst.ML
--- a/src/Tools/IsaPlanner/rw_inst.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Tools/IsaPlanner/rw_inst.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -236,7 +236,7 @@
     |> Drule.implies_intr_list cprems
     |> Drule.forall_intr_list frees_of_fixed_vars
     |> Drule.forall_elim_list vars
-    |> Thm.varifyT_global' othertfrees
+    |> Thm.varifyT_global' (Term_Subst.TFrees.make_set othertfrees)
     |-> K Drule.zero_var_indexes
   end;
 
diff -r 38c01d7e9f5b -r cbbd08df65bd src/Tools/misc_legacy.ML
--- a/src/Tools/misc_legacy.ML	Sat Sep 04 11:22:24 2021 +0100
+++ b/src/Tools/misc_legacy.ML	Tue Sep 07 10:17:03 2021 +0200
@@ -5,6 +5,8 @@
 
 signature MISC_LEGACY =
 sig
+  val thm_frees: thm -> cterm list
+  val cterm_frees: cterm -> cterm list
   val add_term_names: term * string list -> string list
   val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
   val add_term_tfrees: term * (string * sort) list -> (string * sort) list
@@ -24,6 +26,18 @@
 structure Misc_Legacy: MISC_LEGACY =
 struct
 
+fun thm_frees th =
+  (th, (Term_Subst.Frees.empty, [])) |-> Thm.fold_atomic_cterms {hyps = true} Term.is_Free
+    (fn ct => fn (set, list) =>
+      let val v = Term.dest_Free (Thm.term_of ct) in
+        if not (Term_Subst.Frees.defined set v)
+        then (Term_Subst.Frees.add (v, ()) set, ct :: list)
+        else (set, list)
+      end)
+  |> #2;
+
+val cterm_frees = thm_frees o Drule.mk_term;
+
 (*iterate a function over all types in a term*)
 fun it_term_types f =
 let fun iter(Const(_,T), a) = f(T,a)
@@ -235,7 +249,7 @@
 fun freeze_thaw_robust ctxt th =
  let val fth = Thm.legacy_freezeT th
  in
-   case Thm.fold_terms Term.add_vars fth [] of
+   case Thm.fold_terms {hyps = false} Term.add_vars fth [] of
        [] => (fth, fn _ => fn x => x)   (*No vars: nothing to do!*)
      | vars =>
          let fun newName (ix,_) = (ix, gensym (string_of_indexname ix))