--- a/src/HOL/Tools/numeral.ML Tue Sep 18 11:06:22 2007 +0200
+++ b/src/HOL/Tools/numeral.ML Tue Sep 18 16:08:00 2007 +0200
@@ -7,8 +7,8 @@
signature NUMERAL =
sig
- val mk_cnumeral: integer -> cterm
- val mk_cnumber: ctyp -> integer -> cterm
+ val mk_cnumeral: int -> cterm
+ val mk_cnumber: ctyp -> int -> cterm
end;
structure Numeral: NUMERAL =
@@ -23,9 +23,8 @@
fun mk_cnumeral 0 = @{cterm "Numeral.Pls"}
| mk_cnumeral ~1 = @{cterm "Numeral.Min"}
| mk_cnumeral i =
- let val (q, r) = Integer.divmod i 2 in
- Thm.capply (Thm.capply @{cterm "Numeral.Bit"} (mk_cnumeral q))
- (mk_cbit (Integer.machine_int r))
+ let val (q, r) = Integer.div_mod i 2 in
+ Thm.capply (Thm.capply @{cterm "Numeral.Bit"} (mk_cnumeral q)) (mk_cbit r)
end;