diff -r 9003b293e775 -r 156e12d5cb92 src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML
--- a/src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML	Fri May 17 11:35:52 2013 +0200
+++ b/src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML	Fri May 17 13:46:18 2013 +0200
@@ -263,11 +263,11 @@
 fun m_elem_at m i = Inttab.lookup m i
 
 fun v_only_elem v =
-    case Inttab.min_key v of
+    case Inttab.min v of
         NONE => NONE
-      | SOME vmin => (case Inttab.max_key v of
+      | SOME (vmin, _) => (case Inttab.max v of
                           NONE => SOME vmin
-                        | SOME vmax => if vmin = vmax then SOME vmin else NONE)
+                        | SOME (vmax, _) => if vmin = vmax then SOME vmin else NONE)
 
 fun v_fold f = Inttab.fold f;
 fun m_fold f = Inttab.fold f;