--- a/src/FOLP/simpdata.ML Tue Mar 03 19:08:04 2015 +0100
+++ b/src/FOLP/simpdata.ML Wed Mar 04 19:53:18 2015 +0100
@@ -16,7 +16,7 @@
(* Conversion into rewrite rules *)
-fun mk_eq th = case concl_of th of
+fun mk_eq th = case Thm.concl_of th of
_ $ (Const (@{const_name iff}, _) $ _ $ _) $ _ => th
| _ $ (Const (@{const_name eq}, _) $ _ $ _) $ _ => th
| _ $ (Const (@{const_name Not}, _) $ _) $ _ => th RS @{thm not_P_imp_P_iff_F}
@@ -32,7 +32,7 @@
fun mk_atomize pairs =
let fun atoms th =
- (case concl_of th of
+ (case Thm.concl_of th of
Const ("Trueprop", _) $ p =>
(case head_of p of
Const(a,_) =>