--- a/src/HOL/Matrix/cplex/matrixlp.ML Fri Oct 17 10:21:03 2008 +0200
+++ b/src/HOL/Matrix/cplex/matrixlp.ML Fri Oct 17 10:39:39 2008 +0200
@@ -25,7 +25,7 @@
local
-val cert = cterm_of (the_context ())
+val cert = cterm_of @{theory}
in
@@ -72,7 +72,7 @@
"ComputeHOL.compute_bool" "ComputeHOL.compute_pair"
"SparseMatrix.sorted_sp_simps" "ComputeNumeral.number_norm"
"ComputeNumeral.natnorm"};
- val computer = PCompute.make Compute.SML (the_context ()) ths []
+ val computer = PCompute.make Compute.SML @{theory} ths []
in
fun matrix_compute c = hd (PCompute.rewrite computer [c])
@@ -90,7 +90,7 @@
fun prove_bound lptfile prec =
let
- val th = lp_dual_estimate_llprt lptfile prec
+ val th = lp_dual_estimate_prt lptfile prec
in
matrix_simplify th
end