--- 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);