diff -r c85eeff78b33 -r 412a24a4c751 src/Pure/General/integer.ML
--- a/src/Pure/General/integer.ML	Fri Jun 16 14:20:18 2023 +0200
+++ b/src/Pure/General/integer.ML	Sat Jun 17 12:52:45 2023 +0200
@@ -7,6 +7,7 @@
 signature INTEGER =
 sig
   val build: (int -> int) -> int
+  val build1: (int -> int) -> int
   val min: int -> int -> int
   val max: int -> int -> int
   val add: int -> int -> int
@@ -31,6 +32,7 @@
 struct
 
 fun build (f: int -> int) = f 0;
+fun build1 (f: int -> int) = f 1;
 
 fun min x y = Int.min (x, y);
 fun max x y = Int.max (x, y);
@@ -38,8 +40,8 @@
 fun add x y = x + y;
 fun mult x y = x * y;
 
-fun sum xs = fold add xs 0;
-fun prod xs = fold mult xs 1;
+val sum = build o fold add;
+val prod = build1 o fold mult;
 
 fun sign x = int_ord (x, 0);