# HG changeset patch # User wenzelm # Date 1165921426 -3600 # Node ID c4f6bb3920308f91d97f019c7af53820290ed772 # Parent d460465a9f97376e0d1bfd75c4119b27897a319b make SML/NJ happy; diff -r d460465a9f97 -r c4f6bb392030 src/HOL/Tools/numeral_syntax.ML --- a/src/HOL/Tools/numeral_syntax.ML Tue Dec 12 11:57:30 2006 +0100 +++ b/src/HOL/Tools/numeral_syntax.ML Tue Dec 12 12:03:46 2006 +0100 @@ -24,7 +24,7 @@ fun bit b bs = Syntax.const "\\<^const>Numeral.Bit" $ bs $ HOLogic.mk_bit b; fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const "\\<^const>Numeral.Pls") | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const "\\<^const>Numeral.Min") - | mk i = let val (q, r) = IntInf.divMod (i, 2) in bit r (mk q) end; + | mk i = let val (q, r) = IntInf.divMod (i, 2) in bit (IntInf.toInt r) (mk q) end; in mk value end; in