src/ZF/simpdata.ML

--- a/src/ZF/simpdata.ML	Tue Mar 03 19:08:04 2015 +0100
+++ b/src/ZF/simpdata.ML	Wed Mar 04 19:53:18 2015 +0100
@@ -18,7 +18,7 @@
                      SOME rls => maps (atomize (conn_pairs, mem_pairs)) ([th] RL rls)
                    | NONE => [th])
             | _ => [th]
-  in case concl_of th of
+  in case Thm.concl_of th of
          Const(@{const_name Trueprop},_) $ P =>
             (case P of
                  Const(@{const_name mem},_) $ a $ b => tryrules mem_pairs b