diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML
--- a/src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML	Wed Nov 26 16:55:43 2014 +0100
+++ b/src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML	Wed Nov 26 20:05:34 2014 +0100
@@ -80,7 +80,7 @@
         val eupper = HOLogic.mk_prod (index, fupper)
       in (elower :: lower, eupper :: upper) end;
   in
-    pairself (HOLogic.mk_list spvec_elemT) (Inttab.fold app vector ([], []))
+    apply2 (HOLogic.mk_list spvec_elemT) (Inttab.fold app vector ([], []))
   end;
 
 fun approx_matrix prec pprt vector =
@@ -93,7 +93,7 @@
         val eupper = HOLogic.mk_prod (index, fupper)
       in (elower :: lower, eupper :: upper) end;
   in
-    pairself (HOLogic.mk_list spmat_elemT) (Inttab.fold app vector ([], []))
+    apply2 (HOLogic.mk_list spmat_elemT) (Inttab.fold app vector ([], []))
   end;
 
 exception Nat_expected of int;