src/Pure/Tools/codegen_serializer.ML

   let
     fun dest_bit (IConst (c, _)) = if c = c_bit0 then SOME 0
           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;
   in dest_numeral end;