--- 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
--- 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;
--- 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)));
--- 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
--- 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, []);
--- 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)
--- 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
--- 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);
--- 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';
--- 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
--- 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,
--- 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)
--- 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)
--- 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;
--- 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
--- 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;
--- 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;
--- 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;
--- 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)
--- 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 =
--- 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;
--- 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 =
--- 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;
--- 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 = [],
--- 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
--- 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;
--- 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
--- 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;
--- 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;
--- 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 [];
--- 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;
--- 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
--- 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;
--- 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 _ =>