# HG changeset patch
# User haftmann
# Date 1648409272 0
# Node ID 05f7f5454cb6bd40e0490ff2c3e6b7f0024e33d2
# Parent  96c19d03b5a576789af86c4f34bcb7115c18af5d
prefer build combinator

diff -r 96c19d03b5a5 -r 05f7f5454cb6 src/Pure/Isar/code.ML
--- 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
diff -r 96c19d03b5a5 -r 05f7f5454cb6 src/Tools/Code/code_namespace.ML
--- 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;
diff -r 96c19d03b5a5 -r 05f7f5454cb6 src/Tools/Code/code_preproc.ML
--- 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));
diff -r 96c19d03b5a5 -r 05f7f5454cb6 src/Tools/Code/code_printer.ML
--- 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;
 
diff -r 96c19d03b5a5 -r 05f7f5454cb6 src/Tools/Code/code_runtime.ML
--- 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';
diff -r 96c19d03b5a5 -r 05f7f5454cb6 src/Tools/Code/code_scala.ML
--- 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
diff -r 96c19d03b5a5 -r 05f7f5454cb6 src/Tools/Code/code_thingol.ML
--- 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) =