src/HOL/Matrix_LP/matrixlp.ML

--- a/src/HOL/Matrix_LP/matrixlp.ML	Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Matrix_LP/matrixlp.ML	Wed Mar 04 19:53:18 2015 +0100
@@ -23,7 +23,7 @@
 
 fun matrix_simplify th =
   let
-    val simp_th = matrix_compute (cprop_of th)
+    val simp_th = matrix_compute (Thm.cprop_of th)
     val th = Thm.strip_shyps (Thm.equal_elim simp_th th)
     fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle THM _ => th
   in