| changeset 21788 | d460465a9f97 |
| parent 21778 | 66440bf72cdc |
| child 21820 | 2f2b6a965ccc |
--- a/src/HOL/hologic.ML Tue Dec 12 07:46:40 2006 +0100 +++ b/src/HOL/hologic.ML Tue Dec 12 11:57:30 2006 +0100 @@ -327,7 +327,7 @@ | mk_binum ~1 = min_const | mk_binum i = let val (q, r) = IntInf.divMod (i, 2) - in bit_const $ mk_binum q $ mk_bit r end; + in bit_const $ mk_binum q $ mk_bit (IntInf.toInt r) end; fun dest_binum (Const ("Numeral.Pls", _)) = 0 | dest_binum (Const ("Numeral.Min", _)) = ~1