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