src/Pure/General/integer.ML

 Auxiliary operations on (unbounded) integers.
 *)
 
 signature INTEGER =
 sig
+  val build: (int -> int) -> int
   val min: int -> int -> int
   val max: int -> int -> int
   val add: int -> int -> int
   val mult: int -> int -> int
   val sum: int list -> int

   val eval_radix: int -> int list -> int (* base -> coefficients -> value *)
 end;
 
 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);
 
 fun add x y = x + y;

     val _ = if base < 2
       then error ("Bad radix base: " ^ string_of_int base) else ();
     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;