Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
made SML/NJ happy;
authorwenzelm
Tue, 12 Dec 2006 11:57:30 +0100
changeset 21788 d460465a9f97
parent 21787 9edd495b6330
child 21789 c4f6bb392030
made SML/NJ happy;
src/HOL/hologic.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle