author | obua |
Fri, 10 Sep 2004 14:54:54 +0200 | |
changeset 15196 | c7d69df58482 |
parent 15195 | 197e00ce3f20 |
child 15197 | 19e735596e51 |
--- a/src/HOL/Matrix/FloatSparseMatrixBuilder.ML Fri Sep 10 00:19:15 2004 +0200 +++ b/src/HOL/Matrix/FloatSparseMatrixBuilder.ML Fri Sep 10 14:54:54 2004 +0200 @@ -91,7 +91,9 @@ else if n = minus_one then HOLogic.min_const else let - val (q,r) = IntInf.divMod (n, two) + (*val (q,r) = IntInf.divMod (n, two): doesn't work in SML 10.0.7, but in newer versions!!!*) + val q = IntInf.div (n, two) + val r = IntInf.mod (n, two) in HOLogic.bit_const $ bin_of q $ mk_bit r end