tuned: prefer "build" combinator;

--- a/src/Pure/General/integer.ML	Thu Mar 30 16:10:50 2023 +0200
+++ b/src/Pure/General/integer.ML	Sat Apr 01 13:04:59 2023 +0200
@@ -6,6 +6,7 @@
 
 signature INTEGER =
 sig
+  val build: (int -> int) -> int
   val min: int -> int -> int
   val max: int -> int -> int
   val add: int -> int -> int
@@ -29,6 +30,8 @@
 structure Integer : INTEGER =
 struct
 
+fun build (f: int -> int) = f 0;
+
 fun min x y = Int.min (x, y);
 fun max x y = Int.max (x, y);
 
@@ -65,7 +68,7 @@
     fun shift i = swap (div_mod i base);
   in funpow_yield len shift k |> fst end;
 
-fun eval_radix base ks =
-  fold_rev (fn k => fn i => k + i * base) ks 0;
+fun eval_radix base =
+  build o fold_rev (fn k => fn i => k + i * base);
 
 end;

--- a/src/Pure/General/set.ML	Thu Mar 30 16:10:50 2023 +0200
+++ b/src/Pure/General/set.ML	Sat Apr 01 13:04:59 2023 +0200
@@ -82,16 +82,14 @@
 (* size *)
 
 local
-  fun add_size Empty n = n
-    | add_size (Leaf1 _) n = n + 1
-    | add_size (Leaf2 _) n = n + 2
-    | add_size (Leaf3 _) n = n + 3
-    | add_size (Branch2 (left, _, right)) n =
-        n + 1 |> add_size left |> add_size right
-    | add_size (Branch3 (left, _, mid, _, right)) n =
-        n + 2 |> add_size left |> add_size mid |> add_size right;
+  fun count Empty n = n
+    | count (Leaf1 _) n = n + 1
+    | count (Leaf2 _) n = n + 2
+    | count (Leaf3 _) n = n + 3
+    | count (Branch2 (left, _, right)) n = count right (count left (n + 1))
+    | count (Branch3 (left, _, mid, _, right)) n = count right (count mid (count left (n + 2)));
 in
-  fun size set = add_size set 0;
+  val size = Integer.build o count;
 end;
 
 
@@ -131,7 +129,7 @@
           fold_rev left (f e1 (fold_rev mid (f e2 (fold_rev right x))));
   in fold_rev end;
 
-fun dest tab = fold_rev_set cons tab [];
+val dest = Library.build o fold_rev_set cons;
 
 
 (* exists and forall *)

--- a/src/Pure/General/table.ML	Thu Mar 30 16:10:50 2023 +0200
+++ b/src/Pure/General/table.ML	Sat Apr 01 13:04:59 2023 +0200
@@ -164,8 +164,8 @@
           fold_rev left (f e1 (fold_rev mid (f e2 (fold_rev right x))));
   in fold_rev end;
 
-fun dest tab = fold_rev_table cons tab [];
-fun keys tab = fold_rev_table (cons o #1) tab [];
+fun dest tab = Library.build (fold_rev_table cons tab);
+fun keys tab = Library.build (fold_rev_table (cons o #1) tab);
 
 
 (* min/max entries *)

--- a/src/Pure/PIDE/yxml.ML	Thu Mar 30 16:10:50 2023 +0200
+++ b/src/Pure/PIDE/yxml.ML	Sat Apr 01 13:04:59 2023 +0200
@@ -81,8 +81,8 @@
       | tree (XML.Text s) = string s;
   in tree end;
 
-fun tree_size tree = traverse (Integer.add o size) tree 0;
-fun body_size body = fold (Integer.add o tree_size) body 0;
+val tree_size = Integer.build o traverse (Integer.add o size);
+val body_size = Integer.build o fold (Integer.add o tree_size);
 
 
 (* output *)

--- a/src/Pure/ROOT.ML	Thu Mar 30 16:10:50 2023 +0200
+++ b/src/Pure/ROOT.ML	Sat Apr 01 13:04:59 2023 +0200
@@ -38,6 +38,7 @@
 
 ML_file "library.ML";
 ML_file "General/print_mode.ML";
+ML_file "General/integer.ML";
 ML_file "General/alist.ML";
 ML_file "General/table.ML";
 ML_file "General/set.ML";
@@ -64,7 +65,6 @@
 
 subsection "Library of general tools";
 
-ML_file "General/integer.ML";
 ML_file "General/stack.ML";
 ML_file "General/queue.ML";
 ML_file "General/heap.ML";

--- a/src/Pure/Thy/latex.ML	Thu Mar 30 16:10:50 2023 +0200
+++ b/src/Pure/Thy/latex.ML	Sat Apr 01 13:04:59 2023 +0200
@@ -168,8 +168,8 @@
 
 in
 
-fun length_symbols syms =
-  fold Integer.add (these (read scan_latex_length syms)) 0;
+val length_symbols =
+  Integer.build o fold Integer.add o these o read scan_latex_length;
 
 fun output_symbols syms =
   if member (op =) syms Symbol.latex then