--- a/src/HOL/Matrix/cplex/matrixlp.ML Sat May 15 21:41:32 2010 +0200
+++ b/src/HOL/Matrix/cplex/matrixlp.ML Sat May 15 21:50:05 2010 +0200
@@ -81,8 +81,8 @@
fun matrix_simplify th =
let
val simp_th = matrix_compute (cprop_of th)
- val th = Thm.strip_shyps (equal_elim simp_th th)
- fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th (* FIXME avoid handle _ *)
+ val th = Thm.strip_shyps (Thm.equal_elim simp_th th)
+ fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle _ => th (* FIXME avoid handle _ *)
in
removeTrue th
end