--- a/src/Pure/Isar/code.ML Sun Mar 27 19:27:50 2022 +0000
+++ b/src/Pure/Isar/code.ML Sun Mar 27 19:27:52 2022 +0000
@@ -113,7 +113,7 @@
fun devarify ty =
let
- val tys = fold_atyps (fn TVar vi_sort => AList.update (op =) vi_sort) ty [];
+ val tys = build (fold_atyps (fn TVar vi_sort => AList.update (op =) vi_sort) ty);
val vs = Name.invent Name.context Name.aT (length tys);
val mapping = map2 (fn v => fn (vi, sort) => (vi, TFree (v, sort))) vs tys;
in Term.typ_subst_TVars mapping ty end;
@@ -795,7 +795,7 @@
fun desymbolize_tvars thy thms =
let
- val tvs = fold (Term.add_tvars o Thm.prop_of) thms [];
+ val tvs = build (fold (Term.add_tvars o Thm.prop_of) thms);
val instT =
mk_desymbolization (unprefix "'") (prefix "'") (Thm.global_ctyp_of thy o TVar) tvs;
in map (Thm.instantiate (TVars.make instT, Vars.empty)) thms end;
@@ -963,8 +963,8 @@
^ string_of_const thy c ^ "\n" ^ Thm.string_of_thm_global thy thm)) thms;
val tvars_of = build_rev o Term.add_tvarsT;
val vss = map (tvars_of o snd o head_eqn) thms;
- fun inter_sorts vs =
- fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
+ val inter_sorts =
+ build o fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd);
val sorts = map_transpose inter_sorts vss;
val vts = Name.invent_names Name.context Name.aT sorts;
fun instantiate vs =
@@ -1046,7 +1046,7 @@
val equations = if null propers then [] else
Thm.prop_of cert_thm
|> Logic.dest_conjunction_balanced (length propers);
- in (vs, fold (add_rhss_of_eqn thy) equations []) end
+ in (vs, build (fold (add_rhss_of_eqn thy) equations)) end
| typargs_deps_of_cert thy (Projection (t, _)) =
(fst (typscheme_projection thy t), add_rhss_of_eqn thy t [])
| typargs_deps_of_cert thy (Abstract (abs_thm, tyco)) =
@@ -1168,7 +1168,7 @@
in (param, co) end;
fun analyze_cases cases =
let
- val co_list = fold (AList.update (op =) o dest_case) cases [];
+ val co_list = build (fold (AList.update (op =) o dest_case) cases);
in map (AList.lookup (op =) co_list) params end;
fun analyze_let t =
let
--- a/src/Tools/Code/code_namespace.ML Sun Mar 27 19:27:50 2022 +0000
+++ b/src/Tools/Code/code_namespace.ML Sun Mar 27 19:27:52 2022 +0000
@@ -181,7 +181,7 @@
fun build_module_namespace ctxt enforce_upper { module_prefix, module_name, identifiers, reserved } program =
let
- val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program [];
+ val module_names = build (Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program);
val module_fragments' = module_fragments
{ module_name = module_name, identifiers = identifiers, reserved = reserved };
val adjust_case = if enforce_upper then map (Name.enforce_case true) else I;
--- a/src/Tools/Code/code_preproc.ML Sun Mar 27 19:27:50 2022 +0000
+++ b/src/Tools/Code/code_preproc.ML Sun Mar 27 19:27:52 2022 +0000
@@ -201,7 +201,7 @@
let
val t = Thm.term_of ct;
val vs_original =
- fold_term_types (K (fold_atyps (insert (eq_fst op =) o dest_TFree))) t [];
+ build (fold_term_types (K (fold_atyps (insert (eq_fst op =) o dest_TFree))) t);
val vs_normalized = Name.invent_names Name.context Name.aT (map snd vs_original);
val normalize =
map_type_tfree (TFree o the o AList.lookup (op =) (vs_original ~~ vs_normalized));
--- a/src/Tools/Code/code_printer.ML Sun Mar 27 19:27:50 2022 +0000
+++ b/src/Tools/Code/code_printer.ML Sun Mar 27 19:27:52 2022 +0000
@@ -341,7 +341,7 @@
fun gen_print_bind print_term thm (fxy : fixity) pat vars =
let
- val vs = Code_Thingol.fold_varnames (insert (op =)) pat [];
+ val vs = build (Code_Thingol.fold_varnames (insert (op =)) pat);
val vars' = intro_vars vs vars;
in (print_term thm vars' fxy pat, vars') end;
--- a/src/Tools/Code/code_runtime.ML Sun Mar 27 19:27:50 2022 +0000
+++ b/src/Tools/Code/code_runtime.ML Sun Mar 27 19:27:52 2022 +0000
@@ -302,7 +302,7 @@
Ts
|> cons T
|> fold (fold add_typ o snd) typ_signs;
- val required_Ts = fold add_typ requested_Ts [];
+ val required_Ts = build (fold add_typ requested_Ts);
val of_term_for_typ' = of_term_for_typ required_Ts;
val eval_for_const' = eval_for_const ctxt proper_cTs;
val eval_for_const'' = the_default "_" o Option.map eval_for_const';
--- a/src/Tools/Code/code_scala.ML Sun Mar 27 19:27:50 2022 +0000
+++ b/src/Tools/Code/code_scala.ML Sun Mar 27 19:27:52 2022 +0000
@@ -211,8 +211,8 @@
end
| print_def const (vs, ty) eqs =
let
- val tycos = fold (fn ((ts, t), _) =>
- fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
+ val tycos = build (fold (fn ((ts, t), _) =>
+ fold Code_Thingol.add_tyconames (t :: ts)) eqs);
val tyvars = reserved
|> intro_base_names
(is_none o tyco_syntax) deresolve_tyco tycos
--- a/src/Tools/Code/code_thingol.ML Sun Mar 27 19:27:50 2022 +0000
+++ b/src/Tools/Code/code_thingol.ML Sun Mar 27 19:27:52 2022 +0000
@@ -287,12 +287,12 @@
| adjungate_clause ctxt vs_map ts
(body as ICase { term = IVar (SOME v), clauses = clauses, ... }) =
let
- val vs = (fold o fold_varnames) (insert (op =)) ts [];
+ val vs = build ((fold o fold_varnames) (insert (op =)) ts);
fun varnames_disjunctive pat =
- null (inter (op =) vs (fold_varnames (insert (op =)) pat []));
+ null (inter (op =) vs (build (fold_varnames (insert (op =)) pat)));
fun purge_unused_vars_in t =
let
- val vs = fold_varnames (insert (op =)) t [];
+ val vs = build (fold_varnames (insert (op =)) t);
in
map_terms_bottom_up (fn IVar (SOME v) =>
IVar (if member (op =) vs v then SOME v else NONE) | t => t)
@@ -342,8 +342,8 @@
type program = stmt Code_Symbol.Graph.T;
-fun unimplemented program =
- Code_Symbol.Graph.fold (fn (Constant c, (NoStmt, _)) => cons c | _ => I) program [];
+val unimplemented =
+ build o Code_Symbol.Graph.fold (fn (Constant c, (NoStmt, _)) => cons c | _ => I);
fun implemented_deps program =
Code_Symbol.Graph.keys program
@@ -737,7 +737,7 @@
let
val (vs, body) = unfold_abs_eta tys t;
val vs_map =
- fold_index (fn (i, (SOME v, _)) => cons (v, i) | _ => I) vs [];
+ build (fold_index (fn (i, (SOME v, _)) => cons (v, i) | _ => I) vs);
val ts = map (IVar o fst) vs;
in adjungate_clause ctxt vs_map ts body end;
fun mk_clauses [] ty (t, ts_clause) =