make SML/NJ happy;
authorwenzelm
Tue Dec 12 12:03:46 2006 +0100 (2006-12-12)
changeset 21789c4f6bb392030
parent 21788 d460465a9f97
child 21790 9d2761d09d91
make SML/NJ happy;
src/HOL/Tools/numeral_syntax.ML
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Tue Dec 12 11:57:30 2006 +0100
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Tue Dec 12 12:03:46 2006 +0100
     1.3 @@ -24,7 +24,7 @@
     1.4      fun bit b bs = Syntax.const "\\<^const>Numeral.Bit" $ bs $ HOLogic.mk_bit b;
     1.5      fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const "\\<^const>Numeral.Pls")
     1.6        | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const "\\<^const>Numeral.Min")
     1.7 -      | mk i = let val (q, r) = IntInf.divMod (i, 2) in bit r (mk q) end;
     1.8 +      | mk i = let val (q, r) = IntInf.divMod (i, 2) in bit (IntInf.toInt r) (mk q) end;
     1.9    in mk value end;
    1.10  
    1.11  in