diff -r 37d3a984d730 -r 0e52bb862910 src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Sun May 06 13:33:39 2007 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Sun May 06 18:07:04 2007 +0200
@@ -231,12 +231,12 @@
           else if c = c_bit1 then SOME 1
           else NONE
       | dest_bit _ = NONE;
-    fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME 0
-          else if c = c_min then SOME ~1
+    fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME (IntInf.fromInt 0)
+          else if c = c_min then SOME (IntInf.fromInt ~1)
           else NONE
       | dest_numeral (IConst (c, _) `$ t1 `$ t2) =
           if c = c_bit then case (dest_numeral t1, dest_bit t2)
-           of (SOME n, SOME b) => SOME (2 * n + IntInf.fromInt b)
+           of (SOME n, SOME b) => SOME (IntInf.fromInt 2 * n + IntInf.fromInt b)
             | _ => NONE
           else NONE
       | dest_numeral _ = NONE;