diff -r 82382652e5e7 -r f3f02f36a3e2 src/Pure/General/integer.ML
--- a/src/Pure/General/integer.ML	Mon Oct 19 16:47:21 2009 +0200
+++ b/src/Pure/General/integer.ML	Mon Oct 19 21:54:57 2009 +0200
@@ -1,13 +1,16 @@
 (*  Title:      Pure/General/integer.ML
     Author:     Florian Haftmann, TU Muenchen
 
-Unbounded integers.
+Auxiliary operations on (unbounded) integers.
 *)
 
 signature INTEGER =
 sig
+  val add: int -> int -> int
+  val mult: int -> int -> int
+  val sum: int list -> int
+  val prod: int list -> int
   val sign: int -> order
-  val sum: int list -> int
   val div_mod: int -> int -> int * int
   val square: int -> int
   val pow: int -> int -> int (* exponent -> base -> result *)
@@ -20,9 +23,13 @@
 structure Integer : INTEGER =
 struct
 
-fun sign x = int_ord (x, 0);
+fun add x y = x + y;
+fun mult x y = x * y;
 
-fun sum xs = fold (curry op +) xs 0;
+fun sum xs = fold add xs 0;
+fun prod xs = fold mult xs 1;
+
+fun sign x = int_ord (x, 0);
 
 fun div_mod x y = IntInf.divMod (x, y);