src/HOL/Matrix/FloatSparseMatrixBuilder.ML

--- 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