tuned

--- a/src/HOL/Matrix/matrixlp.ML	Fri Feb 10 23:49:17 2012 +0100
+++ b/src/HOL/Matrix/matrixlp.ML	Fri Feb 10 23:56:09 2012 +0100
@@ -51,7 +51,7 @@
     removeTrue th
   end
 
-fun prove_bound lptfile prec = matrix_simplify (lp_dual_estimate_prt lptfile prec);
+val prove_bound = matrix_simplify oo lp_dual_estimate_prt;
 
 val realFromStr = the o Real.fromString;
 fun float2real (x, y) = realFromStr x * Math.pow (2.0, realFromStr y);