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