# HG changeset patch
# User wenzelm
# Date 1631183594 -7200
# Node ID 612b7e0d67215424b740332b85176b08dca24aae
# Parent  633fe7390c9775f743b312bdababe47164a7500c
clarified signature;
clarified modules;

diff -r 633fe7390c97 -r 612b7e0d6721 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Doc/Implementation/Logic.thy	Thu Sep 09 12:33:14 2021 +0200
@@ -585,7 +585,7 @@
   @{define_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
   @{define_ML Thm.implies_intr: "cterm -> thm -> thm"} \\
   @{define_ML Thm.implies_elim: "thm -> thm -> thm"} \\
-  @{define_ML Thm.generalize: "Symtab.set * Symtab.set -> int -> thm -> thm"} \\
+  @{define_ML Thm.generalize: "Names.set * Names.set -> int -> thm -> thm"} \\
   @{define_ML Thm.instantiate: "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
   -> thm -> thm"} \\
   @{define_ML Thm.add_axiom: "Proof.context ->
diff -r 633fe7390c97 -r 612b7e0d6721 src/Doc/Implementation/Proof.thy
--- a/src/Doc/Implementation/Proof.thy	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Doc/Implementation/Proof.thy	Thu Sep 09 12:33:14 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 ->
-  ((ctyp Term_Subst.TVars.table * cterm Term_Subst.Vars.table) * thm list)
+  ((ctyp TVars.table * cterm 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 633fe7390c97 -r 612b7e0d6721 src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Eisbach/match_method.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -173,7 +173,7 @@
 
                   val param_thm = map (Drule.mk_term o Thm.cterm_of ctxt' o Free) abs_nms
                     |> Conjunction.intr_balanced
-                    |> Drule.generalize (Symtab.empty, Symtab.make_set (map fst abs_nms))
+                    |> Drule.generalize (Names.empty, Names.make_set (map fst abs_nms))
                     |> Thm.tag_free_dummy;
 
                   val atts = map (Attrib.attribute ctxt') att;
@@ -453,7 +453,7 @@
 
     val ((_, inst), ctxt'') = Variable.import_inst true [Thm.term_of concl] ctxt';
     val schematic_terms =
-      Term_Subst.Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt'' t)) inst [];
+      Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt'' t)) inst [];
 
     val goal'' = Thm.instantiate ([], schematic_terms) goal';
     val concl' = Thm.instantiate_cterm ([], schematic_terms) concl;
diff -r 633fe7390c97 -r 612b7e0d6721 src/HOL/Library/cconv.ML
--- a/src/HOL/Library/cconv.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Library/cconv.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -147,7 +147,7 @@
              val inst = Thm.match (Drule.cprems_of rule |> hd, mk_concl (Thm.term_of v) eq)
            in
              (Drule.instantiate_normalize inst rule OF
-               [Drule.generalize (Symtab.empty, Symtab.make_set [u]) eq])
+               [Drule.generalize (Names.empty, Names.make_set [u]) eq])
              |> Drule.zero_var_indexes
            end
 
diff -r 633fe7390c97 -r 612b7e0d6721 src/HOL/Library/code_lazy.ML
--- a/src/HOL/Library/code_lazy.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Library/code_lazy.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -122,7 +122,7 @@
         |> Conjunction.intr_balanced
         |> rewrite_rule ctxt [Thm.symmetric (Thm.assume assum)]
         |> Thm.implies_intr assum
-        |> Thm.generalize (Symtab.empty, Symtab.make_set params) 0
+        |> Thm.generalize (Names.empty, Names.make_set params) 0
         |> Axclass.unoverload ctxt
         |> Thm.varifyT_global
       end
@@ -495,7 +495,7 @@
       |> Drule.infer_instantiate' lthy10
          [SOME (Thm.cterm_of lthy10 (Const (\<^const_name>\<open>Pure.dummy_pattern\<close>, HOLogic.unitT --> lazy_type)))]
       |> Thm.generalize
-         (Symtab.make_set (map (fst o dest_TFree) type_args), Symtab.empty)
+         (Names.make_set (map (fst o dest_TFree) type_args), Names.empty)
          (Variable.maxidx_of lthy10 + 1);
 
     val ctr_post = delay_dummy_thm :: map (fn thm => thm RS @{thm sym}) ctrs_lazy_thms
diff -r 633fe7390c97 -r 612b7e0d6721 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -45,7 +45,7 @@
      ('a -> thm -> 'b Seq.seq) -> 'a -> thm -> 'b Seq.seq
   val try_dest_Trueprop : term -> term
 
-  val type_devar : typ Term_Subst.TVars.table -> term -> term
+  val type_devar : typ TVars.table -> term -> term
   val diff_and_instantiate : Proof.context -> thm -> term -> term -> thm
 
   val batter_tac : Proof.context -> int -> tactic
@@ -573,7 +573,7 @@
     val typeval = map (fn (v, T) => (dest_TVar v, Thm.ctyp_of ctxt T)) type_pairing
 
     val typeval_env =
-      Term_Subst.TVars.table (map (apfst dest_TVar) type_pairing)
+      TVars.make (map (apfst dest_TVar) type_pairing)
     (*valuation of term variables*)
     val termval =
       map (apfst (dest_Var o type_devar typeval_env)) term_pairing
diff -r 633fe7390c97 -r 612b7e0d6721 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -852,7 +852,7 @@
                 |> unfold_thms lthy [dtor_ctor];
             in
               (fp_map_thm' RS ctor_cong RS (ctor_dtor RS sym RS trans))
-              |> Drule.generalize (Symtab.empty, Symtab.make_set [y_s])
+              |> Drule.generalize (Names.empty, Names.make_set [y_s])
             end;
 
         val map_thms =
@@ -931,7 +931,7 @@
               |> infer_instantiate' lthy (replicate live NONE @
                 [SOME (Thm.cterm_of lthy (ctorA $ y)), SOME (Thm.cterm_of lthy (ctorB $ z))])
               |> unfold_thms lthy [dtor_ctor]
-              |> Drule.generalize (Symtab.empty, Symtab.make_set [y_s, z_s])
+              |> Drule.generalize (Names.empty, Names.make_set [y_s, z_s])
             end;
 
         val rel_inject_thms =
diff -r 633fe7390c97 -r 612b7e0d6721 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -160,7 +160,7 @@
       val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0));
     in
       Thm.instantiate' [] [SOME (Thm.cterm_of ctxt eq)] split
-      |> Drule.generalize (Symtab.empty, Symtab.make_set [s])
+      |> Drule.generalize (Names.empty, Names.make_set [s])
     end
   | _ => split);
 
diff -r 633fe7390c97 -r 612b7e0d6721 src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -42,7 +42,7 @@
     |> Conjunction.intr_balanced
     |> rewrite_rule ctxt [Thm.symmetric (Thm.assume assum)]
     |> Thm.implies_intr assum
-    |> Thm.generalize (Symtab.empty, Symtab.make_set params) 0
+    |> Thm.generalize (Names.empty, Names.make_set params) 0
     |> Axclass.unoverload ctxt
     |> Thm.varifyT_global
   end;
diff -r 633fe7390c97 -r 612b7e0d6721 src/HOL/Tools/Function/induction_schema.ML
--- a/src/HOL/Tools/Function/induction_schema.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -381,7 +381,7 @@
 
     val res = Conjunction.intr_balanced (map_index project branches)
       |> fold_rev Thm.implies_intr (map Thm.cprop_of newgoals @ steps)
-      |> Drule.generalize (Symtab.empty, Symtab.make_set [Rn])
+      |> Drule.generalize (Names.empty, Names.make_set [Rn])
 
     val nbranches = length branches
     val npres = length pres
diff -r 633fe7390c97 -r 612b7e0d6721 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -78,8 +78,8 @@
     val (instT, lthy2) = lthy1
       |> Variable.declare_names fixed_crel
       |> Variable.importT_inst (param_rel_subst :: args_subst)
-    val args_fixed = (map (Term_Subst.instantiate (instT, Term_Subst.Vars.empty))) args_subst
-    val param_rel_fixed = Term_Subst.instantiate (instT, Term_Subst.Vars.empty) param_rel_subst
+    val args_fixed = (map (Term_Subst.instantiate (instT, Vars.empty))) args_subst
+    val param_rel_fixed = Term_Subst.instantiate (instT, Vars.empty) param_rel_subst
     val rty = (domain_type o fastype_of) param_rel_fixed
     val relcomp_op = Const (\<^const_name>\<open>relcompp\<close>, 
           (rty --> rty' --> HOLogic.boolT) --> 
@@ -295,7 +295,7 @@
     let
       val tvars = rev (subtract op= exclude (fold Term.add_tvars ts []))
       val (tfrees, ctxt') = Variable.invent_types (map #2 tvars) ctxt
-    in (Term_Subst.TVars.table (tvars ~~ map TFree tfrees), ctxt') end
+    in (TVars.make (tvars ~~ map TFree tfrees), ctxt') end
   
   fun import_inst_exclude exclude ts ctxt =
     let
@@ -304,7 +304,7 @@
       val vars = map (apsnd (Term_Subst.instantiateT instT)) 
         (rev (subtract op= exclude (fold Term.add_vars ts [])))
       val (xs, ctxt'') = Variable.variant_fixes (map (#1 o #1) vars) ctxt'
-      val inst = Term_Subst.Vars.table (vars ~~ map Free (xs ~~ map #2 vars))
+      val inst = Vars.make (vars ~~ map Free (xs ~~ map #2 vars))
     in ((instT, inst), ctxt'') end
   
   fun import_terms_exclude exclude ts ctxt =
diff -r 633fe7390c97 -r 612b7e0d6721 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Sep 09 12:33:14 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 (Term_Subst.Vars.dest t_insts)
-    val intro'' = Thm.instantiate (Term_Subst.TVars.dest T_insts, t_insts') intro
+    val t_insts' = map rewrite_pat (Vars.dest t_insts)
+    val intro'' = Thm.instantiate (TVars.dest T_insts, t_insts') intro
     val [intro'''] = Variable.export ctxt3 ctxt [intro'']
     val intro'''' =
       Simplifier.full_simplify
@@ -1072,10 +1072,7 @@
                   " (trying to match " ^ Syntax.string_of_typ ctxt' (fastype_of pred') ^
                   " and " ^ Syntax.string_of_typ ctxt' (fastype_of pred) ^ ")" ^
                   " in " ^ Thm.string_of_thm ctxt' th)
-          in
-            Vartab.fold (fn (xi, (S, T)) => Term_Subst.TVars.add ((xi, S), T))
-              subst Term_Subst.TVars.empty
-          end
+          in TVars.build (Vartab.fold (fn (xi, (S, T)) => TVars.add ((xi, S), T)) subst) end
         fun instantiate_typ th =
           let
             val (pred', _) = strip_intro_concl th
@@ -1084,7 +1081,7 @@
                 raise Fail "Trying to instantiate another predicate"
               else ()
             val instT =
-              Term_Subst.TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt' T))
+              TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt' T))
                 (subst_of (pred', pred)) [];
           in Thm.instantiate (instT, []) th end
         fun instantiate_ho_args th =
@@ -1094,7 +1091,7 @@
             val ho_args' = map dest_Var (ho_args_of_typ T args')
           in Thm.instantiate ([], ho_args' ~~ map (Thm.cterm_of ctxt') ho_args) th end
         val outp_pred =
-          Term_Subst.instantiate (subst_of (inp_pred, pred), Term_Subst.Vars.empty) inp_pred
+          Term_Subst.instantiate (subst_of (inp_pred, pred), Vars.empty) inp_pred
         val ((_, ths'), ctxt1) =
           Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt'
       in
@@ -1163,8 +1160,7 @@
      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 Term_Subst.TFrees.empty t))
+         val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify_global 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 633fe7390c97 -r 612b7e0d6721 src/HOL/Tools/SMT/smt_replay_methods.ML
--- a/src/HOL/Tools/SMT/smt_replay_methods.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_replay_methods.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -171,7 +171,7 @@
 fun by_tac ctxt thms ns ts t tac =
   Goal.prove ctxt [] (map as_prop ts) (as_prop t)
     (fn {context, prems} => HEADGOAL (tac context prems))
-  |> Drule.generalize (Symtab.empty, Symtab.make_set ns)
+  |> Drule.generalize (Names.empty, Names.make_set ns)
   |> discharge 1 thms
 
 fun prove ctxt t tac = by_tac ctxt [] [] [] t (K o tac)
diff -r 633fe7390c97 -r 612b7e0d6721 src/HOL/Tools/Transfer/transfer.ML
--- a/src/HOL/Tools/Transfer/transfer.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -575,7 +575,7 @@
       ((Name.clean_index (prep a, idx), \<^typ>\<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>), Thm.cterm_of ctxt' t)
   in
     thm
-    |> Thm.generalize (Symtab.make_set tfrees, Symtab.make_set (rnames @ frees)) idx
+    |> Thm.generalize (Names.make_set tfrees, Names.make_set (rnames @ frees)) idx
     |> Thm.instantiate (map tinst binsts, map inst binsts)
   end
 
@@ -596,7 +596,7 @@
       ((Name.clean_index (prep a, idx), \<^typ>\<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>), Thm.cterm_of ctxt' t)
   in
     thm
-    |> Thm.generalize (Symtab.make_set tfrees, Symtab.make_set (rnames @ frees)) idx
+    |> Thm.generalize (Names.make_set tfrees, Names.make_set (rnames @ frees)) idx
     |> Thm.instantiate (map tinst binsts, map inst binsts)
   end
 
@@ -719,7 +719,7 @@
     |> Raw_Simplifier.rewrite_rule ctxt' post_simps
     |> Simplifier.norm_hhf ctxt'
     |> Drule.generalize
-        (Symtab.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Symtab.empty)
+        (Names.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Names.empty)
     |> Drule.zero_var_indexes
   end
 (*
@@ -755,7 +755,7 @@
     |> Raw_Simplifier.rewrite_rule ctxt' post_simps
     |> Simplifier.norm_hhf ctxt'
     |> Drule.generalize
-        (Symtab.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Symtab.empty)
+        (Names.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Names.empty)
     |> Drule.zero_var_indexes
   end
 
diff -r 633fe7390c97 -r 612b7e0d6721 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Tools/choice_specification.ML	Thu Sep 09 12:33:14 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 Term_Subst.TFrees.empty prop
+    val (vmap, prop_thawed) = Type.varify_global 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 Term_Subst.TFrees.empty c
+        val (_, c') = Type.varify_global TFrees.empty c
         val (cname,ctyp) = dest_Const c'
       in
         (case filter (fn t =>
diff -r 633fe7390c97 -r 612b7e0d6721 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/General/table.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -406,7 +406,7 @@
 
 (* simultaneous modifications *)
 
-fun make entries = fold update_new entries empty;
+fun make entries = build (fold update_new entries);
 
 fun join f (table1, table2) =
   let
@@ -437,7 +437,7 @@
   modify key (fn NONE => [x] | SOME [] => [x] | SOME (xs as y :: _) =>
     if eq (x, y) then raise SAME else Library.update eq x xs);
 
-fun make_list args = fold_rev cons_list args empty;
+fun make_list args = build (fold_rev cons_list args);
 fun dest_list tab = maps (fn (key, xs) => map (pair key) xs) (dest tab);
 fun merge_list eq = join (fn _ => Library.merge eq);
 
@@ -448,7 +448,7 @@
 
 fun insert_set x = default (x, ());
 fun remove_set x : set -> set = delete_safe x;
-fun make_set entries = fold insert_set entries empty;
+fun make_set xs = build (fold insert_set xs);
 
 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);
diff -r 633fe7390c97 -r 612b7e0d6721 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/Isar/expression.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -191,7 +191,7 @@
       |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T));
     val cert_inst =
       ((map #1 params ~~
-        map (Term_Subst.instantiateT_frees (Term_Subst.TFrees.table instT)) parm_types) ~~ insts'')
+        map (Term_Subst.instantiateT_frees (TFrees.make instT)) parm_types) ~~ insts'')
       |> map_filter (fn (v, t) => if Free v = t then NONE else SOME (v, cert t));
   in
     (Element.instantiate_normalize_morphism (map (apsnd certT) instT, cert_inst) $>
diff -r 633fe7390c97 -r 612b7e0d6721 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/Isar/generic_target.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -95,10 +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 type_tfrees = TFrees.build (TFrees.add_tfreesT (Term.fastype_of u));
     val extra_tfrees =
       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));
+        (fn TFree v => not (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;
 
@@ -261,11 +261,10 @@
 
     val xs = Variable.add_fixed lthy rhs' [];
     val T = Term.fastype_of rhs;
-    val type_tfrees =
-      Term_Subst.TFrees.build (Term_Subst.add_tfreesT T #> fold (Term_Subst.add_tfreesT o #2) xs);
+    val type_tfrees = TFrees.build (TFrees.add_tfreesT T #> fold (TFrees.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));
+        (fn TFree v => not (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;
@@ -323,9 +322,9 @@
       |>> map Logic.dest_type;
 
     val instT =
-      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 [];
+      TVars.build (fold2 (fn a => fn b =>
+        (case a of TVar v => TVars.add (v, b) | _ => I)) tvars tfrees);
+    val cinstT = TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt T)) instT [];
     val cinst =
       map_filter
         (fn (Var (xi, T), t) =>
diff -r 633fe7390c97 -r 612b7e0d6721 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/Isar/local_defs.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -90,7 +90,7 @@
 fun expand defs =
   Drule.implies_intr_list defs
   #> Drule.generalize
-      (Symtab.empty, fold (Symtab.insert_set o #1 o head_of_def o Thm.term_of) defs Symtab.empty)
+      (Names.empty, Names.build (fold (Names.add_set o #1 o head_of_def o Thm.term_of) defs))
   #> funpow (length defs) (fn th => Drule.reflexive_thm RS th);
 
 val expand_term = Envir.expand_term_frees o map (abs_def o Thm.term_of);
diff -r 633fe7390c97 -r 612b7e0d6721 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/Isar/obtain.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -103,11 +103,9 @@
 
 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 frees = Frees.build (t |> Term.fold_aterms (fn Free v => Frees.add_set v | _ => I));
     val T =
-      (case Term_Subst.Frees.get_first (fn ((x, T), ()) => if x = z then SOME T else NONE) frees of
+      (case 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;
@@ -328,16 +326,16 @@
     val terms = map (Drule.mk_term o Thm.cterm_of ctxt o Free) (xs @ ys');
 
     val instT =
-      Term_Subst.TVars.build
+      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
+              if TVars.defined instT v then instT
+              else TVars.add (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 (Term_Subst.TVars.dest instT, []);
+      |> Thm.instantiate (TVars.dest instT, []);
 
     val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt;
     val vars' =
diff -r 633fe7390c97 -r 612b7e0d6721 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/Isar/specification.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -281,7 +281,7 @@
 
     val _ =
       Proof_Display.print_consts int (Position.thread_data ()) lthy5
-        (Term_Subst.Frees.defined (Term_Subst.Frees.build (Term_Subst.add_frees lhs'))) [(x, T)];
+        (Frees.defined (Frees.build (Frees.add_frees lhs'))) [(x, T)];
   in ((lhs, (def_name, th')), lthy5) end;
 
 val definition' = gen_def check_spec_open (K I);
diff -r 633fe7390c97 -r 612b7e0d6721 src/Pure/Isar/subgoal.ML
--- a/src/Pure/Isar/subgoal.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/Isar/subgoal.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -56,9 +56,9 @@
     val text = asms @ (if do_concl then [concl] else []);
 
     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 schematic_terms = Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt3 t)) inst [];
 
-    val schematics = (Term_Subst.TVars.dest schematic_types, schematic_terms);
+    val schematics = (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,7 +88,7 @@
     val ts = map Thm.term_of params;
 
     val prop = Thm.full_prop_of th';
-    val concl_vars = Term_Subst.Vars.build (Term_Subst.add_vars (Logic.strip_imp_concl prop));
+    val concl_vars = Vars.build (Vars.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';
 
@@ -96,7 +96,7 @@
       let
         val ((x, i), T) = v;
         val (U, args) =
-          if Term_Subst.Vars.defined concl_vars v then (T, [])
+          if 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 633fe7390c97 -r 612b7e0d6721 src/Pure/Proof/proof_checker.ML
--- a/src/Pure/Proof/proof_checker.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/Proof/proof_checker.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -77,7 +77,7 @@
         fun thm_of_atom thm Ts =
           let
             val tvars = build_rev (Term.add_tvars (Thm.full_prop_of thm));
-            val (fmap, thm') = Thm.varifyT_global' Term_Subst.TFrees.empty thm;
+            val (fmap, thm') = Thm.varifyT_global' TFrees.empty thm;
             val ctye =
               (tvars @ map (fn ((_, S), ixn) => (ixn, S)) fmap ~~ map (Thm.global_ctyp_of thy) Ts);
           in
diff -r 633fe7390c97 -r 612b7e0d6721 src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -291,11 +291,11 @@
 fun elim_vars mk_default prf =
   let
     val prop = Proofterm.prop_of prf;
-    val tv = Term_Subst.Vars.build (Term_Subst.add_vars prop);
-    val tf = Term_Subst.Frees.build (Term_Subst.add_frees prop);
+    val tv = Vars.build (Vars.add_vars prop);
+    val tf = Frees.build (Frees.add_frees prop);
 
-    fun hidden_variable (Var v) = not (Term_Subst.Vars.defined tv v)
-      | hidden_variable (Free f) = not (Term_Subst.Frees.defined tf f)
+    fun hidden_variable (Var v) = not (Vars.defined tv v)
+      | hidden_variable (Free f) = not (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 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 as Free (x, T)) = if Frees.defined tf (x, T) then t else mk_default' T
+      | elim_varst (t as Var (xi, T)) = if Vars.defined tv (xi, T) then t else mk_default' T
       | elim_varst t = t;
   in
     Proofterm.map_proof_terms (fn t =>
diff -r 633fe7390c97 -r 612b7e0d6721 src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/Tools/rule_insts.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -53,7 +53,7 @@
   error (msg ^ quote (Term.string_of_vname xi) ^ Position.here pos);
 
 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
+  (case 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: " (ai, pos));
 
@@ -71,14 +71,14 @@
     else error_var "Bad sort for instantiation of type variable: " (xi, pos)
   end;
 
-fun make_instT f (tvars: Term_Subst.TVars.set) =
+fun make_instT f (tvars: TVars.set) =
   let
     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;
+  in TVars.fold (add o #1) tvars [] end;
 
 fun make_inst f vars =
   let
@@ -115,20 +115,20 @@
     val (type_insts, term_insts) =
       List.partition (fn (((x, _), _), _) => String.isPrefix "'" x) raw_insts;
 
-    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);
+    val tvars = TVars.build (Thm.fold_terms {hyps = false} TVars.add_tvars thm);
+    val vars = Vars.build (Thm.fold_terms {hyps = false} Vars.add_vars thm);
 
     (*eigen-context*)
     val (_, ctxt1) = ctxt
-      |> 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
+      |> TVars.fold (Variable.declare_internal o Logic.mk_type o TVar o #1) tvars
+      |> 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));
+      Term_Subst.instantiateT (TVars.make (map (read_type ctxt1 tvars) type_insts));
     val vars1 =
-      Vartab.build (vars |> Term_Subst.Vars.fold (fn ((v, T), ()) =>
+      Vartab.build (vars |> Vars.fold (fn ((v, T), ()) =>
         Vartab.insert (K true) (v, instT1 T)));
 
     (*term instantiations*)
@@ -137,12 +137,11 @@
     val ((ts, inferred), ctxt2) = read_terms ss Ts ctxt1;
 
     (*implicit type instantiations*)
-    val instT2 = Term_Subst.instantiateT (Term_Subst.TVars.table inferred);
+    val instT2 = Term_Subst.instantiateT (TVars.make inferred);
     val vars2 = Vartab.fold (fn (v, T) => cons (v, instT2 T)) vars1 [];
     val inst2 =
-      Term_Subst.instantiate (Term_Subst.TVars.empty,
-        Term_Subst.Vars.build
-          (fold2 (fn (xi, _) => fn t => Term_Subst.Vars.add ((xi, Term.fastype_of t), t)) xs ts))
+      Term_Subst.instantiate (TVars.empty,
+        Vars.build (fold2 (fn (xi, _) => fn t => Vars.add ((xi, Term.fastype_of t), t)) xs ts))
       #> Envir.beta_norm;
 
     val inst_tvars = make_instT (instT2 o instT1) tvars;
diff -r 633fe7390c97 -r 612b7e0d6721 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/consts.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -227,9 +227,8 @@
     val declT = type_scheme consts c;
     val args = typargs consts (c, declT);
     val inst =
-      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)]);
+      TVars.build (fold2 (fn a => fn T => 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;
 
 fun dummy_types consts =
diff -r 633fe7390c97 -r 612b7e0d6721 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/drule.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -51,7 +51,7 @@
 sig
   include BASIC_DRULE
   val outer_params: term -> (string * typ) list
-  val generalize: Symtab.set * Symtab.set -> thm -> thm
+  val generalize: Names.set * Names.set -> thm -> thm
   val list_comb: cterm * cterm list -> cterm
   val strip_comb: cterm -> cterm * cterm list
   val beta_conv: cterm -> cterm -> cterm
@@ -179,18 +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 =
-      Term_Subst.Vars.build (th |> (Thm.fold_terms {hyps = false} o Term.fold_aterms)
+      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
+              if 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
+                in Vars.add ((xi, T), ct) inst end
           | _ => inst)));
   in
     th
-    |> Thm.instantiate ([], Term_Subst.Vars.dest inst)
+    |> Thm.instantiate ([], Vars.dest inst)
     |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) ps
   end;
 
@@ -213,16 +213,16 @@
         val (instT, inst) =
           Term_Subst.zero_var_indexes_inst Name.context (map Thm.full_prop_of ths);
 
-        val tvars = fold Thm.add_tvars ths Term_Subst.TVars.empty;
-        val the_tvar = the o Term_Subst.TVars.lookup tvars;
+        val tvars = TVars.build (fold Thm.add_tvars ths);
+        val the_tvar = the o TVars.lookup tvars;
         val instT' =
-          build (instT |> Term_Subst.TVars.fold (fn (v, TVar (b, _)) =>
+          build (instT |> 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 Term_Subst.Vars.empty;
-        val the_var = the o Term_Subst.Vars.lookup vars;
+        val vars = Vars.build (fold (Thm.add_vars o Thm.instantiate (instT', [])) ths);
+        val the_var = the o Vars.lookup vars;
         val inst' =
-          build (inst |> Term_Subst.Vars.fold (fn (v, Var (b, _)) =>
+          build (inst |> 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;
 
diff -r 633fe7390c97 -r 612b7e0d6721 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/goal.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -116,18 +116,18 @@
     val assms = Assumption.all_assms_of ctxt;
     val As = map Thm.term_of assms;
 
-    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 frees = Frees.build (fold Frees.add_frees (prop :: As));
+    val xs = Frees.fold_rev (cons o Thm.cterm_of ctxt o Free o #1) frees [];
 
-    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 tfrees = TFrees.build (fold TFrees.add_tfrees (prop :: As));
+    val Ts = Names.build (TFrees.fold (Names.add_set o #1 o #1) tfrees);
     val instT =
-      build (tfrees |> Term_Subst.TFrees.fold (fn ((a, S), ()) =>
+      build (tfrees |> TFrees.fold (fn ((a, S), ()) =>
         cons (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S)))));
 
     val global_prop =
       Logic.list_implies (As, prop)
-      |> Term_Subst.Frees.fold_rev (Logic.all o Free o #1) frees
+      |> Frees.fold_rev (Logic.all o Free o #1) frees
       |> Logic.varify_types_global
       |> Thm.cterm_of ctxt
       |> Thm.weaken_sorts' ctxt;
@@ -136,7 +136,7 @@
         Drule.implies_intr_list assms #>
         Drule.forall_intr_list xs #>
         Thm.adjust_maxidx_thm ~1 #>
-        Thm.generalize (Ts, Symtab.empty) 0 #>
+        Thm.generalize (Ts, Names.empty) 0 #>
         Thm.strip_shyps #>
         Thm.solve_constraints);
     val local_result =
diff -r 633fe7390c97 -r 612b7e0d6721 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/more_thm.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -25,8 +25,8 @@
   structure Thmtab: TABLE
   val eq_ctyp: ctyp * ctyp -> bool
   val aconvc: cterm * cterm -> bool
-  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 add_tvars: thm -> ctyp TVars.table -> ctyp TVars.table
+  val add_vars: thm -> cterm Vars.table -> cterm Vars.table
   val dest_funT: ctyp -> ctyp * ctyp
   val strip_type: ctyp -> ctyp list * ctyp
   val all_name: Proof.context -> string * cterm -> cterm -> cterm
@@ -140,12 +140,12 @@
 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);
+    in tab |> not (TVars.defined tab v) ? TVars.add (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);
+    in tab |> not (Vars.defined tab v) ? Vars.add (v, ct) end);
 
 
 (* ctyp operations *)
@@ -414,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 = 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 tfrees = Names.build (fold (Names.add_set o #1 o #1) instT);
+        val frees = Names.build (fold (Names.add_set o #1 o #1) inst);
 
         val hyps = Thm.chyps_of th;
         val inst_cterm =
@@ -454,11 +454,11 @@
 fun forall_intr_vars th =
   let
     val (_, vars) =
-      (th, (Term_Subst.Vars.empty, [])) |-> Thm.fold_atomic_cterms {hyps = false} Term.is_Var
+      (th, (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)
+            if not (Vars.defined seen v)
+            then (Vars.add_set v seen, ct :: vars)
             else (seen, vars)
           end);
   in fold Thm.forall_intr vars th end;
@@ -466,15 +466,15 @@
 fun forall_intr_frees th =
   let
     val fixed =
-      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));
+      Frees.build
+       (fold Frees.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th)) #>
+        fold Frees.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)
+            if not (Frees.defined seen v)
+            then (Frees.add_set v seen, ct :: frees)
             else (seen, frees)
           end);
   in fold Thm.forall_intr frees th end;
@@ -492,23 +492,23 @@
     val certT = Thm.global_ctyp_of thy;
 
     val instT =
-      Term_Subst.TVars.build (prop |> (Term.fold_types o Term.fold_atyps)
+      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
+              if TVars.defined instT v then instT
+              else TVars.add (v, TFree (a, S)) instT
           | _ => instT)));
-    val cinstT = Term_Subst.TVars.map (K certT) instT;
+    val cinstT = TVars.map (K certT) instT;
     val cinst =
-      Term_Subst.Vars.build (prop |> Term.fold_aterms
+      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
+              in Vars.add (((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;
+  in Thm.instantiate (TVars.dest cinstT, Vars.dest cinst) th end;
 
 fun unvarify_axiom thy = unvarify_global thy o Thm.axiom thy;
 
diff -r 633fe7390c97 -r 612b7e0d6721 src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/morphism.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -137,17 +137,13 @@
 fun instantiate_frees_morphism ([], []) = identity
   | instantiate_frees_morphism (cinstT, cinst) =
       let
-        val instT =
-          Term_Subst.TFrees.build
-            (cinstT |> fold (fn (v, cT) => Term_Subst.TFrees.add (v, Thm.typ_of cT)));
-        val inst =
-          Term_Subst.Frees.build
-            (cinst |> fold (fn (v, ct) => Term_Subst.Frees.add (v, Thm.term_of ct)));
+        val instT = TFrees.build (cinstT |> fold (fn (v, cT) => TFrees.add (v, Thm.typ_of cT)));
+        val inst = Frees.build (cinst |> fold (fn (v, ct) => Frees.add (v, Thm.term_of ct)));
       in
         morphism "instantiate_frees"
           {binding = [],
            typ =
-            if Term_Subst.TFrees.is_empty instT then []
+            if TFrees.is_empty instT then []
             else [Term_Subst.instantiateT_frees instT],
            term = [Term_Subst.instantiate_frees (instT, inst)],
            fact = [map (Thm.instantiate_frees (cinstT, cinst))]}
@@ -156,17 +152,13 @@
 fun instantiate_morphism ([], []) = identity
   | instantiate_morphism (cinstT, cinst) =
       let
-        val instT =
-          Term_Subst.TVars.build (cinstT |> fold (fn (v, cT) =>
-            Term_Subst.TVars.add (v, Thm.typ_of cT)));
-        val inst =
-          Term_Subst.Vars.build (cinst |> fold (fn (v, ct) =>
-            Term_Subst.Vars.add (v, Thm.term_of ct)));
+        val instT = TVars.build (cinstT |> fold (fn (v, cT) => TVars.add (v, Thm.typ_of cT)));
+        val inst = Vars.build (cinst |> fold (fn (v, ct) => Vars.add (v, Thm.term_of ct)));
       in
         morphism "instantiate"
           {binding = [],
            typ =
-            if Term_Subst.TVars.is_empty instT then []
+            if TVars.is_empty instT then []
             else [Term_Subst.instantiateT instT],
            term = [Term_Subst.instantiate (instT, inst)],
            fact = [map (Thm.instantiate (cinstT, cinst))]}
diff -r 633fe7390c97 -r 612b7e0d6721 src/Pure/primitive_defs.ML
--- a/src/Pure/primitive_defs.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/primitive_defs.ML	Thu Sep 09 12:33:14 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_Subst.TFrees.build (Term_Subst.add_tfrees head);
+    val head_tfrees = TFrees.build (TFrees.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 Term_Subst.TFrees.defined head_tfrees (a, S) then I
+      if check_tfree a orelse TFrees.defined head_tfrees (a, S) then I
       else insert (op =) v | _ => I)) rhs [];
   in
     if not (check_head head) then
diff -r 633fe7390c97 -r 612b7e0d6721 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/proofterm.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -109,12 +109,12 @@
   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 -> Term_Subst.TFrees.set -> proof -> proof
+  val varify_proof: term -> 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
-  val generalize_proof: Symtab.set * Symtab.set -> int -> term -> proof -> proof
-  val instantiate: typ Term_Subst.TVars.table * term Term_Subst.Vars.table -> proof -> proof
+  val generalize_proof: Names.set * Names.set -> int -> term -> proof -> proof
+  val instantiate: typ TVars.table * term Vars.table -> proof -> proof
   val lift_proof: term -> int -> term -> proof -> proof
   val incr_indexes: int -> proof -> proof
   val assumption_proof: term list -> term -> int -> proof -> proof
@@ -678,8 +678,8 @@
     (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
+          if TVars.defined instT v orelse can (Type.lookup envT) v then instT
+          else TVars.add (v, Logic.dummy_tfree S) instT
       | _ => instT));
 
 fun conflicting_tvars env =
@@ -687,18 +687,18 @@
     (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
+          if Vars.defined inst v orelse can (Envir.lookup env) v then inst
+          else Vars.add (v, Free ("dummy", T)) inst
       | _ => inst));
 
 fun del_conflicting_tvars envT ty =
-  Term_Subst.instantiateT (Term_Subst.TVars.build (conflicting_tvarsT envT ty)) ty;
+  Term_Subst.instantiateT (TVars.build (conflicting_tvarsT envT ty)) ty;
 
 fun del_conflicting_vars env tm =
   let
     val instT =
-      Term_Subst.TVars.build (tm |> Term.fold_types (conflicting_tvarsT (Envir.type_env env)));
-    val inst = Term_Subst.Vars.build (tm |> conflicting_tvars env);
+      TVars.build (tm |> Term.fold_types (conflicting_tvarsT (Envir.type_env env)));
+    val inst = Vars.build (tm |> conflicting_tvars env);
   in Term_Subst.instantiate (instT, inst) tm end;
 
 in
@@ -903,7 +903,7 @@
   let
     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));
+        (fn TFree v => if 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);
@@ -970,14 +970,14 @@
 fun generalize_proof (tfrees, frees) idx prop prf =
   let
     val gen =
-      if Symtab.is_empty frees then []
+      if Names.is_empty frees then []
       else
-        fold_aterms (fn Free (x, T) => Symtab.defined frees x ? insert (op =) (x, T) | _ => I)
-          (Term_Subst.generalize (tfrees, Symtab.empty) idx prop) [];
+        fold_aterms (fn Free (x, T) => Names.defined frees x ? insert (op =) (x, T) | _ => I)
+          (Term_Subst.generalize (tfrees, Names.empty) idx prop) [];
   in
     prf
     |> Same.commit (map_proof_terms_same
-        (Term_Subst.generalize_same (tfrees, Symtab.empty) idx)
+        (Term_Subst.generalize_same (tfrees, Names.empty) idx)
         (Term_Subst.generalizeT_same tfrees idx))
     |> fold (fn (x, T) => forall_intr_proof (x, Free (x, T)) NONE) gen
     |> fold_rev (fn (x, T) => fn prf' => prf' %> Var (Name.clean_index (x, idx), T)) gen
@@ -988,7 +988,7 @@
 
 fun instantiate (instT, inst) =
   Same.commit (map_proof_terms_same
-    (Term_Subst.instantiate_same (instT, Term_Subst.Vars.map (K remove_types) inst))
+    (Term_Subst.instantiate_same (instT, Vars.map (K remove_types) inst))
     (Term_Subst.instantiateT_same instT));
 
 
diff -r 633fe7390c97 -r 612b7e0d6721 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/raw_simplifier.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -161,13 +161,13 @@
 fun rewrite_rule_extra_vars prems elhs erhs =
   let
     val elhss = elhs :: prems;
-    val tvars = Term_Subst.TVars.build (fold Term_Subst.add_tvars elhss);
-    val vars = Term_Subst.Vars.build (fold Term_Subst.add_vars elhss);
+    val tvars = TVars.build (fold TVars.add_tvars elhss);
+    val vars = Vars.build (fold Vars.add_vars elhss);
   in
     erhs |> Term.exists_type (Term.exists_subtype
-      (fn TVar v => not (Term_Subst.TVars.defined tvars v) | _ => false)) orelse
+      (fn TVar v => not (TVars.defined tvars v) | _ => false)) orelse
     erhs |> Term.exists_subterm
-      (fn Var v => not (Term_Subst.Vars.defined vars v) | _ => false)
+      (fn Var v => not (Vars.defined vars v) | _ => false)
   end;
 
 fun rrule_extra_vars elhs thm =
@@ -474,7 +474,7 @@
     (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;
+val vars_set = Vars.build o Vars.add_vars;
 
 local
 
@@ -483,7 +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 Term_Subst.Vars.eq_set (apply2 vars_set (t, u));
+fun var_perm (t, u) = vperm (t, u) andalso Vars.eq_set (apply2 vars_set (t, u));
 
 in
 
@@ -946,7 +946,7 @@
   while the premises are solved.*)
 
 fun cond_skel (args as (_, (lhs, rhs))) =
-  if Term_Subst.Vars.subset (vars_set rhs, vars_set lhs) then uncond_skel args
+  if Vars.subset (vars_set rhs, vars_set lhs) then uncond_skel args
   else skel0;
 
 (*
diff -r 633fe7390c97 -r 612b7e0d6721 src/Pure/term_ord.ML
--- a/src/Pure/term_ord.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/term_ord.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -5,6 +5,70 @@
 Term orderings and scalable collections.
 *)
 
+signature ITEMS =
+sig
+  type key
+  type 'a table
+  val empty: 'a table
+  val build: ('a table -> 'a table) -> 'a table
+  val is_empty: '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 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: 'a table -> key -> 'a option
+  val defined: 'a table -> key -> bool
+  val add: key * 'a -> 'a table -> 'a table
+  val make: (key * 'a) list -> 'a table
+  type set = unit table
+  val add_set: key -> set -> set
+  val make_set: key list -> set
+  val subset: set * set -> bool
+  val eq_set: set * set -> bool
+end;
+
+functor Items(Key: KEY): ITEMS =
+struct
+
+structure Table = Table(Key);
+
+type key = Table.key;
+type 'a table = 'a Table.table;
+
+val empty = Table.empty;
+val build = Table.build;
+val is_empty = Table.is_empty;
+val size = Table.size;
+val dest = Table.dest;
+val keys = Table.keys;
+val exists = Table.exists;
+val forall = Table.forall;
+val get_first = Table.get_first;
+val lookup = Table.lookup;
+val defined = Table.defined;
+
+fun add entry = Table.insert (K true) entry;
+fun make entries = Table.build (fold add entries);
+
+type set = unit table;
+
+fun add_set x = add (x, ());
+fun make_set xs = build (fold add_set xs);
+
+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);
+
+val map = Table.map;
+val fold = Table.fold;
+val fold_rev = Table.fold_rev;
+
+end;
+
 signature BASIC_TERM_ORD =
 sig
   structure Vartab: TABLE
@@ -15,6 +79,35 @@
   structure Sort_Graph: GRAPH
   structure Typ_Graph: GRAPH
   structure Term_Graph: GRAPH
+  structure TFrees:
+  sig
+    include ITEMS
+    val add_tfreesT: typ -> set -> set
+    val add_tfrees: term -> set -> set
+  end
+  structure TVars:
+  sig
+    include ITEMS
+    val add_tvarsT: typ -> set -> set
+    val add_tvars: term -> set -> set
+  end
+  structure Frees:
+  sig
+    include ITEMS
+    val add_frees: term -> set -> set
+  end
+  structure Vars:
+  sig
+    include ITEMS
+    val add_vars: term -> set -> set
+  end
+  structure Names:
+  sig
+    include ITEMS
+    val add_tfree_namesT: typ -> set -> set
+    val add_tfree_names: term -> set -> set
+    val add_free_names: term -> set -> set
+  end
 end;
 
 signature TERM_ORD =
@@ -221,12 +314,55 @@
 structure Typtab = Table(type key = typ val ord = typ_ord);
 structure Termtab = Table(type key = term val ord = fast_term_ord);
 
+fun term_cache f = Cache.create Termtab.empty Termtab.lookup Termtab.update f;
+
 structure Var_Graph = Graph(type key = indexname val ord = fast_indexname_ord);
 structure Sort_Graph = Graph(type key = sort val ord = sort_ord);
 structure Typ_Graph = Graph(type key = typ val ord = typ_ord);
 structure Term_Graph = Graph(type key = term val ord = fast_term_ord);
 
-fun term_cache f = Cache.create Termtab.empty Termtab.lookup Termtab.update f;
+structure TFrees =
+struct
+  structure Items =
+    Items(type key = string * sort val ord = pointer_eq_ord (prod_ord fast_string_ord sort_ord));
+  open Items;
+  val add_tfreesT = fold_atyps (fn TFree v => add_set v | _ => I);
+  val add_tfrees = fold_types add_tfreesT;
+end;
+
+structure TVars =
+struct
+  structure Items =
+    Items(type key = indexname * sort val ord = pointer_eq_ord (prod_ord fast_indexname_ord sort_ord));
+  open Items;
+  val add_tvarsT = fold_atyps (fn TVar v => add_set v | _ => I);
+  val add_tvars = fold_types add_tvarsT;
+end;
+
+structure Frees =
+struct
+  structure Items =
+    Items(type key = string * typ val ord = pointer_eq_ord (prod_ord fast_string_ord typ_ord));
+  open Items;
+  val add_frees = fold_aterms (fn Free v => add_set v | _ => I);
+end;
+
+structure Vars =
+struct
+  structure Items =
+    Items(type key = indexname * typ val ord = pointer_eq_ord (prod_ord fast_indexname_ord typ_ord));
+  open Items;
+  val add_vars = fold_aterms (fn Var v => add_set v | _ => I);
+end;
+
+structure Names =
+struct
+  structure Items = Items(type key = string val ord = fast_string_ord);
+  open Items;
+  val add_tfree_namesT = fold_atyps (fn TFree (a, _) => add_set a | _ => I);
+  val add_tfree_names = fold_types add_tfree_namesT;
+  val add_free_names = fold_aterms (fn Free (x, _) => add_set x | _ => I);
+end;
 
 end;
 
diff -r 633fe7390c97 -r 612b7e0d6721 src/Pure/term_subst.ML
--- a/src/Pure/term_subst.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/term_subst.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -4,47 +4,15 @@
 Efficient type/term substitution.
 *)
 
-signature INST_TABLE =
-sig
-  include TABLE
-  val add: key * 'a -> 'a table -> 'a table
-  val table: (key * 'a) list -> 'a table
-end;
-
-functor Inst_Table(Key: KEY): INST_TABLE =
-struct
-
-structure Tab = Table(Key);
-
-fun add entry = Tab.insert (K true) entry;
-fun table entries = Tab.build (fold add entries);
-
-open Tab;
-
-end;
-
 signature TERM_SUBST =
 sig
-  structure TFrees: INST_TABLE
-  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
-  val generalizeT_same: Symtab.set -> int -> typ Same.operation
-  val generalize_same: Symtab.set * Symtab.set -> int -> term Same.operation
-  val generalizeT: Symtab.set -> int -> typ -> typ
-  val generalize: Symtab.set * Symtab.set -> int -> term -> term
+  val generalizeT_same: Names.set -> int -> typ Same.operation
+  val generalize_same: Names.set * Names.set -> int -> term Same.operation
+  val generalizeT: Names.set -> int -> typ -> typ
+  val generalize: Names.set * Names.set -> int -> term -> term
   val instantiateT_maxidx: (typ * int) TVars.table -> typ -> int -> typ * int
   val instantiate_maxidx: (typ * int) TVars.table * (term * int) Vars.table ->
     term -> int -> term * int
@@ -64,39 +32,6 @@
 structure Term_Subst: TERM_SUBST =
 struct
 
-(* instantiation as table *)
-
-structure TFrees = Inst_Table(
-  type key = string * sort
-  val ord = pointer_eq_ord (prod_ord fast_string_ord Term_Ord.sort_ord)
-);
-
-structure TVars = Inst_Table(
-  type key = indexname * sort
-  val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.sort_ord)
-);
-
-structure Frees = Inst_Table(
-  type key = string * typ
-  val ord = pointer_eq_ord (prod_ord fast_string_ord Term_Ord.typ_ord)
-);
-
-structure Vars = Inst_Table(
-  type key = indexname * typ
-  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 *)
 
 fun map_atypsT_same f =
@@ -128,23 +63,23 @@
 (* generalization of fixed variables *)
 
 fun generalizeT_same tfrees idx ty =
-  if Symtab.is_empty tfrees then raise Same.SAME
+  if Names.is_empty tfrees then raise Same.SAME
   else
     let
       fun gen (Type (a, Ts)) = Type (a, Same.map gen Ts)
         | gen (TFree (a, S)) =
-            if Symtab.defined tfrees a then TVar ((a, idx), S)
+            if Names.defined tfrees a then TVar ((a, idx), S)
             else raise Same.SAME
         | gen _ = raise Same.SAME;
     in gen ty end;
 
 fun generalize_same (tfrees, frees) idx tm =
-  if Symtab.is_empty tfrees andalso Symtab.is_empty frees then raise Same.SAME
+  if Names.is_empty tfrees andalso Names.is_empty frees then raise Same.SAME
   else
     let
       val genT = generalizeT_same tfrees idx;
       fun gen (Free (x, T)) =
-            if Symtab.defined frees x then
+            if Names.defined frees x then
               Var (Name.clean_index (x, idx), Same.commit genT T)
             else Free (x, genT T)
         | gen (Var (xi, T)) = Var (xi, genT T)
diff -r 633fe7390c97 -r 612b7e0d6721 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/theory.ML	Thu Sep 09 12:33:14 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 = Term_Subst.TFrees.build (snd lhs |> fold Term_Subst.add_tfreesT);
+    val lhs_vars = TFrees.build (snd lhs |> fold TFrees.add_tfreesT);
     val rhs_extras =
       build (rhs |> fold (#2 #> (fold o Term.fold_atyps)
-        (fn TFree v => not (Term_Subst.TFrees.defined lhs_vars v) ? insert (op =) v | _ => I)));
+        (fn TFree v => not (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 633fe7390c97 -r 612b7e0d6721 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/thm.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -151,9 +151,9 @@
   val equal_elim: thm -> thm -> thm
   val solve_constraints: thm -> thm
   val flexflex_rule: Proof.context option -> thm -> thm Seq.seq
-  val generalize: Symtab.set * Symtab.set -> int -> thm -> thm
-  val generalize_cterm: Symtab.set * Symtab.set -> int -> cterm -> cterm
-  val generalize_ctyp: Symtab.set -> int -> ctyp -> ctyp
+  val generalize: Names.set * Names.set -> int -> thm -> thm
+  val generalize_cterm: Names.set * Names.set -> int -> cterm -> cterm
+  val generalize_ctyp: Names.set -> int -> ctyp -> ctyp
   val instantiate: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
     thm -> thm
   val instantiate_cterm: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
@@ -161,7 +161,7 @@
   val trivial: cterm -> thm
   val of_class: ctyp * class -> thm
   val unconstrainT: thm -> thm
-  val varifyT_global': Term_Subst.TFrees.set -> thm -> ((string * sort) * indexname) list * thm
+  val varifyT_global': TFrees.set -> thm -> ((string * sort) * indexname) list * thm
   val varifyT_global: thm -> thm
   val legacy_freezeT: thm -> thm
   val plain_prop_of: thm -> term
@@ -1547,16 +1547,16 @@
 *)
 
 fun generalize (tfrees, frees) idx th =
-  if Symtab.is_empty tfrees andalso Symtab.is_empty frees then th
+  if Names.is_empty tfrees andalso Names.is_empty frees then th
   else
     let
       val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th;
       val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]);
 
       val bad_type =
-        if Symtab.is_empty tfrees then K false
-        else Term.exists_subtype (fn TFree (a, _) => Symtab.defined tfrees a | _ => false);
-      fun bad_term (Free (x, T)) = bad_type T orelse Symtab.defined frees x
+        if Names.is_empty tfrees then K false
+        else Term.exists_subtype (fn TFree (a, _) => Names.defined tfrees a | _ => false);
+      fun bad_term (Free (x, T)) = bad_type T orelse Names.defined frees x
         | bad_term (Var (_, T)) = bad_type T
         | bad_term (Const (_, T)) = bad_type T
         | bad_term (Abs (_, T, t)) = bad_type T orelse bad_term t
@@ -1582,7 +1582,7 @@
     end;
 
 fun generalize_cterm (tfrees, frees) idx (ct as Cterm {cert, t, T, maxidx, sorts}) =
-  if Symtab.is_empty tfrees andalso Symtab.is_empty frees then ct
+  if Names.is_empty tfrees andalso Names.is_empty frees then ct
   else if idx <= maxidx then raise CTERM ("generalize_cterm: bad index", [ct])
   else
     Cterm {cert = cert, sorts = sorts,
@@ -1591,7 +1591,7 @@
       maxidx = Int.max (maxidx, idx)};
 
 fun generalize_ctyp tfrees idx (cT as Ctyp {cert, T, maxidx, sorts}) =
-  if Symtab.is_empty tfrees then cT
+  if Names.is_empty tfrees then cT
   else if idx <= maxidx then raise CTERM ("generalize_ctyp: bad index", [])
   else
     Ctyp {cert = cert, sorts = sorts,
@@ -1616,11 +1616,11 @@
 val add_inst_sorts = add_sorts (fn Cterm {sorts, ...} => sorts);
 
 fun add_instT thy (v as (_, S), Ctyp {T = U, maxidx, ...}) =
-  if Sign.of_sort thy (U, S) then Term_Subst.TVars.add (v, (U, maxidx))
+  if Sign.of_sort thy (U, S) then TVars.add (v, (U, maxidx))
   else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy S, [U], []);
 
 fun add_inst thy (v as (_, T), Cterm {t = u, T = U, maxidx, ...}) =
-  if T = U then Term_Subst.Vars.add (v, (u, maxidx))
+  if T = U then Vars.add (v, (u, maxidx))
   else
     let
       fun pretty_typing t ty =
@@ -1645,8 +1645,8 @@
       |> fold add_instT_sorts instT
       |> fold add_inst_sorts inst;
 
-    val instT' = Term_Subst.TVars.build (fold (add_instT thy') instT);
-    val inst' = Term_Subst.Vars.build (fold (add_inst thy') inst);
+    val instT' = TVars.build (fold (add_instT thy') instT);
+    val inst' = Vars.build (fold (add_inst thy') inst);
   in ((instT', inst'), (cert', sorts')) end;
 
 in
@@ -1669,13 +1669,11 @@
 
         val thy' = Context.certificate_theory cert';
         val constraints' =
-          Term_Subst.TVars.fold (fn ((_, S), (T, _)) => insert_constraints thy' (T, S))
+          TVars.fold (fn ((_, S), (T, _)) => insert_constraints thy' (T, S))
             instT' constraints;
       in
         Thm (deriv_rule1
-          (fn d =>
-            Proofterm.instantiate
-              (Term_Subst.TVars.map (K #1) instT', Term_Subst.Vars.map (K #1) inst') d) der,
+          (fn d => Proofterm.instantiate (TVars.map (K #1) instT', Vars.map (K #1) inst') d) der,
          {cert = cert',
           tags = [],
           maxidx = maxidx',
@@ -1780,7 +1778,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_Subst.add_tfrees hyps fixed;
+    val tfrees = fold TFrees.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);
@@ -1796,7 +1794,7 @@
       prop = prop3}))
   end;
 
-val varifyT_global = #2 o varifyT_global' Term_Subst.TFrees.empty;
+val varifyT_global = #2 o varifyT_global' TFrees.empty;
 
 (*Replace all TVars by TFrees that are often new*)
 fun legacy_freezeT (Thm (der, {cert, constraints, shyps, hyps, tpairs, prop, ...})) =
diff -r 633fe7390c97 -r 612b7e0d6721 src/Pure/type.ML
--- a/src/Pure/type.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/type.ML	Thu Sep 09 12:33:14 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: Term_Subst.TFrees.set -> term -> ((string * sort) * indexname) list * term
+  val varify_global: 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)
@@ -357,7 +357,7 @@
   let
     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));
+        (fn TFree v => if 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));
diff -r 633fe7390c97 -r 612b7e0d6721 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/type_infer.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -114,10 +114,10 @@
         let
           val [a] = Name.invent used Name.aT 1;
           val used' = Name.declare a used;
-        in (Term_Subst.TVars.add ((xi, S), TFree (a, improve_sort S)) inst, used') end
+        in (TVars.add ((xi, S), TFree (a, improve_sort S)) inst, used') end
       else (inst, used);
     val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt);
-    val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) (Term_Subst.TVars.empty, used);
+    val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) (TVars.empty, used);
   in (map o map_types) (Term_Subst.instantiateT inst) ts end;
 
 end;
diff -r 633fe7390c97 -r 612b7e0d6721 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/variable.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -69,15 +69,15 @@
   val export: Proof.context -> Proof.context -> thm list -> thm list
   val export_morphism: Proof.context -> Proof.context -> morphism
   val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context
-  val importT_inst: term list -> Proof.context -> typ Term_Subst.TVars.table * Proof.context
+  val importT_inst: term list -> Proof.context -> typ TVars.table * Proof.context
   val import_inst: bool -> term list -> Proof.context ->
-    (typ Term_Subst.TVars.table * term Term_Subst.Vars.table) * Proof.context
+    (typ TVars.table * term 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 -> (ctyp Term_Subst.TVars.table * thm list) * Proof.context
+  val importT: thm list -> Proof.context -> (ctyp 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 ->
-    ((ctyp Term_Subst.TVars.table * cterm Term_Subst.Vars.table) * thm list) * Proof.context
+    ((ctyp TVars.table * cterm 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
@@ -515,14 +515,14 @@
     val still_fixed = not o is_newly_fixed inner outer;
 
     val gen_fixes =
-      Symtab.build (fixes_of inner |> Name_Space.fold_table (fn (y, _) =>
-        not (is_fixed outer y) ? Symtab.insert_set y));
+      Names.build (fixes_of inner |> Name_Space.fold_table (fn (y, _) =>
+        not (is_fixed outer y) ? Names.add_set y));
 
     val type_occs_inner = type_occs_of inner;
     fun gen_fixesT ts =
-      Symtab.build (fold decl_type_occs ts type_occs_inner |> Symtab.fold (fn (a, xs) =>
+      Names.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));
+        then I else Names.add_set a));
   in (gen_fixesT, gen_fixes) end;
 
 fun exportT_inst inner outer = #1 (export_inst inner outer);
@@ -533,7 +533,7 @@
     val maxidx = maxidx_of outer;
   in
     fn ts => ts |> map
-      (Term_Subst.generalize (mk_tfrees ts, Symtab.empty)
+      (Term_Subst.generalize (mk_tfrees ts, Names.empty)
         (fold (Term.fold_types Term.maxidx_typ) ts maxidx + 1))
   end;
 
@@ -564,7 +564,7 @@
     val idx = fold Thm.maxidx_thm ths maxidx + 1;
   in map (Thm.generalize (tfrees, frees) idx) ths end;
 
-fun exportT inner outer = gen_export (exportT_inst inner outer, Symtab.empty) (maxidx_of outer);
+fun exportT inner outer = gen_export (exportT_inst inner outer, Names.empty) (maxidx_of outer);
 fun export inner outer = gen_export (export_inst inner outer) (maxidx_of outer);
 
 fun export_morphism inner outer =
@@ -592,9 +592,7 @@
   let
     val tvars = build_rev (fold Term.add_tvars ts);
     val (tfrees, ctxt') = invent_types (map #2 tvars) ctxt;
-    val instT =
-      Term_Subst.TVars.build (fold2 (fn a => fn b =>
-        Term_Subst.TVars.add (a, TFree b)) tvars tfrees);
+    val instT = TVars.build (fold2 (fn a => fn b => TVars.add (a, TFree b)) tvars tfrees);
   in (instT, ctxt') end;
 
 fun import_inst is_open ts ctxt =
@@ -603,14 +601,12 @@
     val (instT, ctxt') = importT_inst ts ctxt;
     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 =
-      Term_Subst.Vars.build (fold2 (fn (x, T) => fn y =>
-        Term_Subst.Vars.add ((x, T), Free (y, T))) vars ys);
+    val inst = Vars.build (fold2 (fn (x, T) => fn y => Vars.add ((x, T), Free (y, T))) vars ys);
   in ((instT, inst), ctxt'') end;
 
 fun importT_terms ts ctxt =
   let val (instT, ctxt') = importT_inst ts ctxt
-  in (map (Term_Subst.instantiate (instT, Term_Subst.Vars.empty)) ts, ctxt') end;
+  in (map (Term_Subst.instantiate (instT, Vars.empty)) ts, ctxt') end;
 
 fun import_terms is_open ts ctxt =
   let val (inst, ctxt') = import_inst is_open ts ctxt
@@ -619,8 +615,8 @@
 fun importT ths ctxt =
   let
     val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
-    val instT' = Term_Subst.TVars.map (K (Thm.ctyp_of ctxt')) instT;
-    val ths' = map (Thm.instantiate (Term_Subst.TVars.dest instT', [])) ths;
+    val instT' = TVars.map (K (Thm.ctyp_of ctxt')) instT;
+    val ths' = map (Thm.instantiate (TVars.dest instT', [])) ths;
   in ((instT', ths'), ctxt') end;
 
 fun import_prf is_open prf ctxt =
@@ -632,9 +628,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.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;
+    val instT' = TVars.map (K (Thm.ctyp_of ctxt')) instT;
+    val inst' = Vars.map (K (Thm.cterm_of ctxt')) inst;
+    val ths' = map (Thm.instantiate (TVars.dest instT', Vars.dest inst')) ths;
   in (((instT', inst'), ths'), ctxt') end;
 
 fun import_vars ctxt th =
@@ -690,10 +686,10 @@
 
 fun focus_subgoal bindings i st =
   let
-    val all_vars = Term_Subst.Vars.build (Thm.fold_terms {hyps = false} Term_Subst.add_vars st);
+    val all_vars = Vars.build (Thm.fold_terms {hyps = false} Vars.add_vars st);
   in
-    Term_Subst.Vars.fold (unbind_term o #1 o #1) all_vars #>
-    Term_Subst.Vars.fold (declare_constraints o Var o #1) all_vars #>
+    Vars.fold (unbind_term o #1 o #1) all_vars #>
+    Vars.fold (declare_constraints o Var o #1) all_vars #>
     focus_cterm bindings (Thm.cprem_of st i)
   end;
 
@@ -732,14 +728,14 @@
     val occs = type_occs_of ctxt;
     val occs' = type_occs_of ctxt';
     val types =
-      Symtab.build (occs' |> Symtab.fold (fn (a, _) =>
-        if Symtab.defined occs a then I else Symtab.insert_set a));
+      Names.build (occs' |> Symtab.fold (fn (a, _) =>
+        if Symtab.defined occs a then I else Names.add_set a));
     val idx = maxidx_of ctxt' + 1;
     val Ts' = (fold o fold_types o fold_atyps)
       (fn T as TFree _ =>
           (case Term_Subst.generalizeT types idx T of TVar v => insert (op =) v | _ => I)
         | _ => I) ts [];
-    val ts' = map (Term_Subst.generalize (types, Symtab.empty) idx) ts;
+    val ts' = map (Term_Subst.generalize (types, Names.empty) idx) ts;
   in (rev Ts', ts') end;
 
 fun polymorphic ctxt ts = snd (polymorphic_types ctxt ts);
diff -r 633fe7390c97 -r 612b7e0d6721 src/Tools/IsaPlanner/rw_inst.ML
--- a/src/Tools/IsaPlanner/rw_inst.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML	Thu Sep 09 12:33:14 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' (Term_Subst.TFrees.make_set othertfrees)
+    |> Thm.varifyT_global' (TFrees.make_set othertfrees)
     |-> K Drule.zero_var_indexes
   end;
 
diff -r 633fe7390c97 -r 612b7e0d6721 src/Tools/misc_legacy.ML
--- a/src/Tools/misc_legacy.ML	Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Tools/misc_legacy.ML	Thu Sep 09 12:33:14 2021 +0200
@@ -27,11 +27,11 @@
 struct
 
 fun thm_frees th =
-  (th, (Term_Subst.Frees.empty, [])) |-> Thm.fold_atomic_cterms {hyps = true} Term.is_Free
+  (th, (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)
+        if not (Frees.defined set v)
+        then (Frees.add_set v set, ct :: list)
         else (set, list)
       end)
   |> #2;