# HG changeset patch
# User wenzelm
# Date 1630783508 -7200
# Node ID 1091880266e5088b17a839cebe12bf0db1541f15
# Parent  b3c65c984210933dd167025bb3332eeac5282654
clarified signature;

diff -r b3c65c984210 -r 1091880266e5 src/Pure/General/graph_display.ML
--- a/src/Pure/General/graph_display.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/General/graph_display.ML	Sat Sep 04 21:25:08 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 b3c65c984210 -r 1091880266e5 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/General/table.ML	Sat Sep 04 21:25:08 2021 +0200
@@ -19,6 +19,7 @@
   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
@@ -85,6 +86,8 @@
 
 val empty = Empty;
 
+fun build (f: 'a table -> 'a table) = f empty;
+
 fun is_empty Empty = true
   | is_empty _ = false;
 
diff -r b3c65c984210 -r 1091880266e5 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/Isar/class.ML	Sat Sep 04 21:25:08 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 b3c65c984210 -r 1091880266e5 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/Isar/generic_target.ML	Sat Sep 04 21:25:08 2021 +0200
@@ -95,7 +95,7 @@
     val u = fold_rev lambda term_params rhs';
     val global_rhs = singleton (Variable.polymorphic thy_ctxt) u;
 
-    val type_tfrees = Term_Subst.add_tfreesT (Term.fastype_of u) Term_Subst.TFrees.empty;
+    val type_tfrees = Term_Subst.TFrees.build (Term_Subst.add_tfreesT (Term.fastype_of u));
     val extra_tfrees =
       (u, []) |-> (Term.fold_types o Term.fold_atyps)
         (fn TFree v => not (Term_Subst.TFrees.defined type_tfrees v) ? insert (op =) v | _ => I)
@@ -263,9 +263,7 @@
     val xs = Variable.add_fixed lthy rhs' [];
     val T = Term.fastype_of rhs;
     val type_tfrees =
-      Term_Subst.TFrees.empty
-      |> Term_Subst.add_tfreesT T
-      |> fold (Term_Subst.add_tfreesT o #2) xs;
+      Term_Subst.TFrees.build (Term_Subst.add_tfreesT T #> fold (Term_Subst.add_tfreesT o #2) xs);
     val extra_tfrees =
       (rhs, []) |-> (Term.fold_types o Term.fold_atyps)
         (fn TFree v => not (Term_Subst.TFrees.defined type_tfrees v) ? insert (op =) v | _ => I)
@@ -327,8 +325,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 b3c65c984210 -r 1091880266e5 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/Isar/obtain.ML	Sat Sep 04 21:25:08 2021 +0200
@@ -104,8 +104,8 @@
 fun mk_all_internal ctxt (y, z) t =
   let
     val frees =
-      (t, Term_Subst.Frees.empty)
-      |-> Term.fold_aterms (fn Free v => Term_Subst.Frees.add (v, ()) | _ => I);
+      Term_Subst.Frees.build (t |> Term.fold_aterms
+        (fn Free v => Term_Subst.Frees.add (v, ()) | _ => I));
     val T =
       (case Term_Subst.Frees.get_first (fn ((x, T), ()) => if x = z then SOME T else NONE) frees of
         SOME T => T
@@ -328,12 +328,13 @@
     val terms = map (Drule.mk_term o Thm.cterm_of ctxt o Free) (xs @ ys');
 
     val instT =
-      (params, Term_Subst.TVars.empty) |-> fold (#2 #> Term.fold_atyps (fn T => fn instT =>
-        (case T of
-          TVar v =>
-            if Term_Subst.TVars.defined instT v then instT
-            else Term_Subst.TVars.update (v, Thm.ctyp_of ctxt (norm_type T)) instT
-        | _ => instT)));
+      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 (Term_Subst.TVars.dest instT, []);
diff -r b3c65c984210 -r 1091880266e5 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/Isar/overloading.ML	Sat Sep 04 21:25:08 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 b3c65c984210 -r 1091880266e5 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Sep 04 21:25:08 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 b3c65c984210 -r 1091880266e5 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/Isar/specification.ML	Sat Sep 04 21:25:08 2021 +0200
@@ -281,7 +281,7 @@
 
     val _ =
       Proof_Display.print_consts int (Position.thread_data ()) lthy5
-        (Term_Subst.Frees.defined (Term_Subst.add_frees lhs' Term_Subst.Frees.empty)) [(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 b3c65c984210 -r 1091880266e5 src/Pure/Isar/subgoal.ML
--- a/src/Pure/Isar/subgoal.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/Isar/subgoal.ML	Sat Sep 04 21:25:08 2021 +0200
@@ -88,7 +88,7 @@
     val ts = map Thm.term_of params;
 
     val prop = Thm.full_prop_of th';
-    val concl_vars = Term_Subst.add_vars (Logic.strip_imp_concl prop) Term_Subst.Vars.empty;
+    val concl_vars = Term_Subst.Vars.build (Term_Subst.add_vars (Logic.strip_imp_concl prop));
     val vars = rev (Term.add_vars prop []);
     val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
 
diff -r b3c65c984210 -r 1091880266e5 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/PIDE/document.ML	Sat Sep 04 21:25:08 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 b3c65c984210 -r 1091880266e5 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/PIDE/resources.ML	Sat Sep 04 21:25:08 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 b3c65c984210 -r 1091880266e5 src/Pure/Proof/proof_checker.ML
--- a/src/Pure/Proof/proof_checker.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/Proof/proof_checker.ML	Sat Sep 04 21:25:08 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)
diff -r b3c65c984210 -r 1091880266e5 src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Sat Sep 04 21:25:08 2021 +0200
@@ -291,8 +291,8 @@
 fun elim_vars mk_default prf =
   let
     val prop = Proofterm.prop_of prf;
-    val tv = Term_Subst.add_vars prop Term_Subst.Vars.empty;
-    val tf = Term_Subst.add_frees prop Term_Subst.Frees.empty;
+    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 (Term_Subst.Vars.defined tv v)
       | hidden_variable (Free f) = not (Term_Subst.Frees.defined tf f)
diff -r b3c65c984210 -r 1091880266e5 src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/Syntax/ast.ML	Sat Sep 04 21:25:08 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 b3c65c984210 -r 1091880266e5 src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/Tools/find_consts.ML	Sat Sep 04 21:25:08 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 b3c65c984210 -r 1091880266e5 src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/Tools/rule_insts.ML	Sat Sep 04 21:25:08 2021 +0200
@@ -98,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;
 
@@ -115,8 +115,8 @@
     val (type_insts, term_insts) =
       List.partition (fn (((x, _), _), _) => String.isPrefix "'" x) raw_insts;
 
-    val tvars = Thm.fold_terms Term_Subst.add_tvars thm Term_Subst.TVars.empty;
-    val vars = Thm.fold_terms Term_Subst.add_vars thm Term_Subst.Vars.empty;
+    val tvars = Term_Subst.TVars.build (Thm.fold_terms Term_Subst.add_tvars thm);
+    val vars = Term_Subst.Vars.build (Thm.fold_terms Term_Subst.add_vars thm);
 
     (*eigen-context*)
     val (_, ctxt1) = ctxt
@@ -128,8 +128,8 @@
     val instT1 =
       Term_Subst.instantiateT (Term_Subst.TVars.table (map (read_type ctxt1 tvars) type_insts));
     val vars1 =
-      Term_Subst.Vars.fold (fn ((v, T), ()) => Vartab.insert (K true) (v, instT1 T))
-        vars Vartab.empty;
+      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;
@@ -141,8 +141,8 @@
     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 = make_instT (instT2 o instT1) tvars;
diff -r b3c65c984210 -r 1091880266e5 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/consts.ML	Sat Sep 04 21:25:08 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 b3c65c984210 -r 1091880266e5 src/Pure/defs.ML
--- a/src/Pure/defs.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/defs.ML	Sat Sep 04 21:25:08 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;
 
 
diff -r b3c65c984210 -r 1091880266e5 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/drule.ML	Sat Sep 04 21:25:08 2021 +0200
@@ -185,7 +185,7 @@
       |> map (fn (x, T) => Var ((x, maxidx + 1), Logic.incr_tvar (maxidx + 1) T));
     val Ts = map Term.fastype_of ps;
     val inst =
-      (th, Term_Subst.Vars.empty) |-> (Thm.fold_terms o Term.fold_aterms)
+      Term_Subst.Vars.build (th |> (Thm.fold_terms o Term.fold_aterms)
         (fn t => fn inst =>
           (case t of
             Var (xi, T) =>
@@ -193,7 +193,7 @@
               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));
+          | _ => inst)));
   in
     th
     |> Thm.instantiate ([], Term_Subst.Vars.dest inst)
diff -r b3c65c984210 -r 1091880266e5 src/Pure/envir.ML
--- a/src/Pure/envir.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/envir.ML	Sat Sep 04 21:25:08 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 b3c65c984210 -r 1091880266e5 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/global_theory.ML	Sat Sep 04 21:25:08 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 b3c65c984210 -r 1091880266e5 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/goal.ML	Sat Sep 04 21:25:08 2021 +0200
@@ -120,7 +120,7 @@
     val fixes = map (Thm.cterm_of ctxt) xs;
 
     val tfrees = fold Term.add_tfrees (prop :: As) [];
-    val tfrees_set = fold (Symtab.insert_set o #1) tfrees Symtab.empty;
+    val tfrees_set = Symtab.build (fold (Symtab.insert_set o #1) tfrees);
     val instT = map (fn (a, S) => (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S)))) tfrees;
 
     val global_prop =
diff -r b3c65c984210 -r 1091880266e5 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/more_thm.ML	Sat Sep 04 21:25:08 2021 +0200
@@ -408,8 +408,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 =
@@ -449,9 +449,9 @@
 fun forall_intr_frees th =
   let
     val fixed =
-      Term_Subst.Frees.empty
-      |> fold Term_Subst.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th))
-      |> fold Term_Subst.add_frees (Thm.hyps_of th);
+      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 =
       Thm.fold_atomic_cterms (fn a =>
         (case Thm.term_of a of
@@ -472,22 +472,22 @@
     val certT = Thm.global_ctyp_of thy;
 
     val instT =
-      (prop, Term_Subst.TVars.empty) |-> (Term.fold_types o Term.fold_atyps)
+      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));
+          | _ => instT)));
     val cinstT = Term_Subst.TVars.map (K certT) instT;
     val cinst =
-      (prop, Term_Subst.Vars.empty) |-> Term.fold_aterms
+      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));
+          | _ => 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;
diff -r b3c65c984210 -r 1091880266e5 src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/morphism.ML	Sat Sep 04 21:25:08 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 b3c65c984210 -r 1091880266e5 src/Pure/primitive_defs.ML
--- a/src/Pure/primitive_defs.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/primitive_defs.ML	Sat Sep 04 21:25:08 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.add_tfrees head Term_Subst.TFrees.empty;
+    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
diff -r b3c65c984210 -r 1091880266e5 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/proofterm.ML	Sat Sep 04 21:25:08 2021 +0200
@@ -692,12 +692,13 @@
       | _ => inst));
 
 fun del_conflicting_tvars envT ty =
-  Term_Subst.instantiateT (conflicting_tvarsT envT ty Term_Subst.TVars.empty) ty;
+  Term_Subst.instantiateT (Term_Subst.TVars.build (conflicting_tvarsT envT ty)) ty;
 
 fun del_conflicting_vars env tm =
   let
-    val instT = Term.fold_types (conflicting_tvarsT (Envir.type_env env)) tm Term_Subst.TVars.empty;
-    val inst = conflicting_tvars env tm Term_Subst.Vars.empty;
+    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);
   in Term_Subst.instantiate (instT, inst) tm end;
 
 in
@@ -2144,7 +2145,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
@@ -2325,7 +2326,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 b3c65c984210 -r 1091880266e5 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/raw_simplifier.ML	Sat Sep 04 21:25:08 2021 +0200
@@ -161,8 +161,8 @@
 fun rewrite_rule_extra_vars prems elhs erhs =
   let
     val elhss = elhs :: prems;
-    val tvars = fold Term_Subst.add_tvars elhss Term_Subst.TVars.empty;
-    val vars = fold Term_Subst.add_vars elhss Term_Subst.Vars.empty;
+    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 (Term_Subst.TVars.defined tvars v) | _ => false)) orelse
@@ -474,7 +474,7 @@
     (cond_warning ctxt (fn () => print_thm ctxt "Ignoring duplicate rewrite rule:" ("", thm));
       ctxt));
 
-fun vars_set t = Term_Subst.add_vars t Term_Subst.Vars.empty;
+val vars_set = Term_Subst.Vars.build o Term_Subst.add_vars;
 
 local
 
diff -r b3c65c984210 -r 1091880266e5 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/sorts.ML	Sat Sep 04 21:25:08 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;
 
 
@@ -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 b3c65c984210 -r 1091880266e5 src/Pure/term_subst.ML
--- a/src/Pure/term_subst.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/term_subst.ML	Sat Sep 04 21:25:08 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;
 
@@ -275,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 b3c65c984210 -r 1091880266e5 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/theory.ML	Sat Sep 04 21:25:08 2021 +0200
@@ -244,7 +244,7 @@
         [] => (item, map Logic.varifyT_global args)
       | vs => raise TYPE ("Illegal schematic type variable(s)", map TVar vs, []));
 
-    val lhs_vars = fold Term_Subst.add_tfreesT (snd lhs) Term_Subst.TFrees.empty;
+    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 Term_Subst.TFrees.defined lhs_vars v then I else insert (op =) v)) rhs [];
diff -r b3c65c984210 -r 1091880266e5 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/thm.ML	Sat Sep 04 21:25:08 2021 +0200
@@ -1641,8 +1641,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
@@ -2093,7 +2093,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;
 
diff -r b3c65c984210 -r 1091880266e5 src/Pure/thm_deps.ML
--- a/src/Pure/thm_deps.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/thm_deps.ML	Sat Sep 04 21:25:08 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 b3c65c984210 -r 1091880266e5 src/Pure/type.ML
--- a/src/Pure/type.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/type.ML	Sat Sep 04 21:25:08 2021 +0200
@@ -446,7 +446,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 +474,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 b3c65c984210 -r 1091880266e5 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/variable.ML	Sat Sep 04 21:25:08 2021 +0200
@@ -516,14 +516,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);
@@ -594,8 +594,8 @@
     val tvars = 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 =
@@ -605,8 +605,8 @@
     val vars = map (apsnd (Term_Subst.instantiateT instT)) (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 =
@@ -690,9 +690,7 @@
   in ((xs ~~ ps', goal'), ctxt') end;
 
 fun focus_subgoal bindings i st =
-  let
-    val all_vars = Thm.fold_terms Term_Subst.add_vars st Term_Subst.Vars.empty;
-  in
+  let val all_vars = Term_Subst.Vars.build (Thm.fold_terms Term_Subst.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 #>
     focus_cterm bindings (Thm.cprem_of st i)
@@ -733,8 +731,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 _ =>