# HG changeset patch
# User haftmann
# Date 1328914569 -3600
# Node ID 9673597c1b92ada636ea5acab5dcd2fb8939b4c1
# Parent  5522e28a566e7584df163821aa35f7dda1e4cf73
tuned

diff -r 5522e28a566e -r 9673597c1b92 src/HOL/Matrix/matrixlp.ML
--- 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);