--- a/src/Sequents/simpdata.ML Tue Mar 03 19:08:04 2015 +0100
+++ b/src/Sequents/simpdata.ML Wed Mar 04 19:53:18 2015 +0100
@@ -12,7 +12,7 @@
(*Make atomic rewrite rules*)
fun atomize r =
- case concl_of r of
+ case Thm.concl_of r of
Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) =>
(case (Cla.forms_of_seq a, Cla.forms_of_seq c) of
([], [p]) =>
@@ -28,7 +28,7 @@
| _ => [r];
(*Make meta-equalities.*)
-fun mk_meta_eq ctxt th = case concl_of th of
+fun mk_meta_eq ctxt th = case Thm.concl_of th of
Const(@{const_name Pure.eq},_)$_$_ => th
| Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) =>
(case (Cla.forms_of_seq a, Cla.forms_of_seq c) of