# HG changeset patch
# User wenzelm
# Date 1630785935 -7200
# Node ID 4f2bd13edce3be77987e434afe130f5224f6a784
# Parent  9eff7c673b42cc996a2789fcb2e1edceaea95636
clarified signature;

diff -r 9eff7c673b42 -r 4f2bd13edce3 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sat Sep 04 21:45:43 2021 +0200
+++ b/src/Pure/Isar/generic_target.ML	Sat Sep 04 22:05:35 2021 +0200
@@ -97,9 +97,8 @@
 
     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)
-      |> rev;
+      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));
     val type_params = map (Logic.mk_type o TFree) extra_tfrees;
   in (global_rhs, (extra_tfrees, (type_params, term_params))) end;
 
@@ -265,9 +264,8 @@
     val type_tfrees =
       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)
-      |> rev;
+      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));
     val mx' = check_mixfix lthy (b, extra_tfrees) mx;
 
     val type_params = map (Logic.mk_type o TFree) extra_tfrees;
diff -r 9eff7c673b42 -r 4f2bd13edce3 src/Pure/System/options.ML
--- a/src/Pure/System/options.ML	Sat Sep 04 21:45:43 2021 +0200
+++ b/src/Pure/System/options.ML	Sat Sep 04 22:05:35 2021 +0200
@@ -156,8 +156,8 @@
 fun encode (Options tab) =
   let
     val opts =
-      (tab, []) |-> Symtab.fold (fn (name, {pos, typ, value}) =>
-        cons (Position.properties_of pos, (name, (typ, value))));
+      build (tab |> Symtab.fold (fn (name, {pos, typ, value}) =>
+        cons (Position.properties_of pos, (name, (typ, value)))));
     open XML.Encode;
   in list (pair properties (pair string (pair string string))) opts end;
 
diff -r 9eff7c673b42 -r 4f2bd13edce3 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Sat Sep 04 21:45:43 2021 +0200
+++ b/src/Pure/Thy/export_theory.ML	Sat Sep 04 22:05:35 2021 +0200
@@ -172,7 +172,7 @@
         val parent_spaces = map get_space parents;
         val space = get_space thy;
       in
-        (decls, []) |-> fold (fn (name, decl) =>
+        build (decls |> fold (fn (name, decl) =>
           if exists (fn space => Name_Space.declared space name) parent_spaces then I
           else
             (case export name decl of
@@ -181,7 +181,7 @@
                 let
                   val i = #serial (Name_Space.the_entry space name);
                   val body = if enabled then make_body () else [];
-                in cons (i, XML.Elem (entity_markup space name, body)) end))
+                in cons (i, XML.Elem (entity_markup space name, body)) end)))
         |> sort (int_ord o apply2 #1) |> map #2
         |> export_body thy export_name
       end;
diff -r 9eff7c673b42 -r 4f2bd13edce3 src/Pure/context.ML
--- a/src/Pure/context.ML	Sat Sep 04 21:45:43 2021 +0200
+++ b/src/Pure/context.ML	Sat Sep 04 22:05:35 2021 +0200
@@ -466,10 +466,10 @@
 end;
 
 fun theory_data_size thy =
-  (data_of thy, []) |-> Datatab.fold_rev (fn (k, _) =>
+  build (data_of thy |> Datatab.fold_rev (fn (k, _) =>
     (case Theory_Data.obj_size k thy of
       NONE => I
-    | SOME n => (cons (invoke_pos k, n))));
+    | SOME n => (cons (invoke_pos k, n)))));
 
 
 
diff -r 9eff7c673b42 -r 4f2bd13edce3 src/Pure/defs.ML
--- a/src/Pure/defs.ML	Sat Sep 04 21:45:43 2021 +0200
+++ b/src/Pure/defs.ML	Sat Sep 04 22:05:35 2021 +0200
@@ -148,10 +148,10 @@
         NONE => false
       | SOME {specs, ...} => Inttab.defined specs i));
   in
-    (defs, []) |-> Itemtab.fold (fn (c, {specs, ...}) =>
+    build (defs |> Itemtab.fold (fn (c, {specs, ...}) =>
       specs |> Inttab.fold (fn (i, spec) =>
         if #1 c = Const andalso is_some (#def spec) andalso not (prev_spec c i)
-        then cons (#2 c, the (#def spec)) else I))
+        then cons (#2 c, the (#def spec)) else I)))
   end;
 
 val empty = Defs Itemtab.empty;
diff -r 9eff7c673b42 -r 4f2bd13edce3 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sat Sep 04 21:45:43 2021 +0200
+++ b/src/Pure/drule.ML	Sat Sep 04 22:05:35 2021 +0200
@@ -222,14 +222,14 @@
         val tvars = fold Thm.add_tvars ths [];
         fun the_tvar v = the (find_first (fn cT => v = dest_TVar (Thm.typ_of cT)) tvars);
         val instT' =
-          (instT, []) |-> Term_Subst.TVars.fold (fn (v, TVar (b, _)) =>
-            cons (v, Thm.rename_tvar b (the_tvar v)));
+          build (instT |> Term_Subst.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 [];
         fun the_var v = the (find_first (fn ct => v = dest_Var (Thm.term_of ct)) vars);
         val inst' =
-          (inst, []) |-> Term_Subst.Vars.fold (fn (v, Var (b, _)) =>
-            cons (v, Thm.var (b, Thm.ctyp_of_cterm (the_var v))));
+          build (inst |> Term_Subst.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;
 
 val zero_var_indexes = singleton zero_var_indexes_list;
diff -r 9eff7c673b42 -r 4f2bd13edce3 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Sat Sep 04 21:45:43 2021 +0200
+++ b/src/Pure/facts.ML	Sat Sep 04 22:05:35 2021 +0200
@@ -217,7 +217,8 @@
 fun consolidate facts =
   let
     val unfinished =
-      (facts, []) |-> fold_static_lazy (fn (_, ths) => if Lazy.is_finished ths then I else cons ths);
+      build (facts |> fold_static_lazy (fn (_, ths) =>
+        if Lazy.is_finished ths then I else cons ths));
     val _ = Lazy.consolidate unfinished;
   in facts end;
 
diff -r 9eff7c673b42 -r 4f2bd13edce3 src/Pure/library.ML
--- a/src/Pure/library.ML	Sat Sep 04 21:45:43 2021 +0200
+++ b/src/Pure/library.ML	Sat Sep 04 22:05:35 2021 +0200
@@ -51,6 +51,8 @@
   val forall: ('a -> bool) -> 'a list -> bool
 
   (*lists*)
+  val build: ('a list -> 'a list) -> 'a list
+  val build_rev: ('a list -> 'a list) -> 'a list
   val single: 'a -> 'a list
   val the_single: 'a list -> 'a
   val singleton: ('a list -> 'b list) -> 'a -> 'b
@@ -301,6 +303,9 @@
 
 (** lists **)
 
+fun build (f: 'a list -> 'a list) = f [];
+fun build_rev f = build f |> rev;
+
 fun single x = [x];
 
 fun the_single [x] = x
diff -r 9eff7c673b42 -r 4f2bd13edce3 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Sep 04 21:45:43 2021 +0200
+++ b/src/Pure/proofterm.ML	Sat Sep 04 22:05:35 2021 +0200
@@ -902,8 +902,8 @@
 fun varify_proof t fixed prf =
   let
     val fs =
-      (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);
+      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));
     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);
diff -r 9eff7c673b42 -r 4f2bd13edce3 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Sat Sep 04 21:45:43 2021 +0200
+++ b/src/Pure/sorts.ML	Sat Sep 04 22:05:35 2021 +0200
@@ -299,16 +299,16 @@
   let
     fun new_classrel rel = not (exists (fn algebra => class_less algebra rel) parents);
     val classrel =
-      (classes, []) |-> Graph.fold (fn (c, (_, (_, ds))) =>
+      build (classes |> Graph.fold (fn (c, (_, (_, ds))) =>
         (case filter (fn d => new_classrel (c, d)) (Graph.Keys.dest ds) of
           [] => I
-        | ds' => cons (c, sort_strings ds')))
+        | ds' => cons (c, sort_strings ds'))))
       |> sort_by #1;
 
     fun is_arity t ar algebra = member (op =) (Symtab.lookup_list (arities_of algebra) t) ar;
     fun add_arity t (c, Ss) = not (exists (is_arity t (c, Ss)) parents) ? cons (t, Ss, c);
     val arities =
-      (arities, []) |-> Symtab.fold (fn (t, ars) => fold_rev (add_arity t) (sort_by #1 ars))
+      build (arities |> Symtab.fold (fn (t, ars) => fold_rev (add_arity t) (sort_by #1 ars)))
       |> sort_by #1;
   in {classrel = classrel, arities = arities} end;
 
diff -r 9eff7c673b42 -r 4f2bd13edce3 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Sep 04 21:45:43 2021 +0200
+++ b/src/Pure/thm.ML	Sat Sep 04 22:05:35 2021 +0200
@@ -2300,8 +2300,8 @@
 (* type arities *)
 
 fun thynames_of_arity thy (a, c) =
-  (get_arities thy, []) |-> Aritytab.fold
-    (fn ((a', _, c'), (_, name, ser)) => (a = a' andalso c = c') ? cons (name, ser))
+  build (get_arities thy |> Aritytab.fold
+    (fn ((a', _, c'), (_, name, ser)) => (a = a' andalso c = c') ? cons (name, ser)))
   |> sort (int_ord o apply2 #2) |> map #1;
 
 fun insert_arity_completions thy ((t, Ss, c), (th, thy_name, ser)) (finished, arities) =
diff -r 9eff7c673b42 -r 4f2bd13edce3 src/Pure/type.ML
--- a/src/Pure/type.ML	Sat Sep 04 21:45:43 2021 +0200
+++ b/src/Pure/type.ML	Sat Sep 04 22:05:35 2021 +0200
@@ -356,8 +356,8 @@
 fun varify_global fixed t =
   let
     val fs =
-      (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);
+      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));
     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));