--- a/src/Sequents/simpdata.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Sequents/simpdata.ML Fri Sep 25 20:37:59 2015 +0200
@@ -38,7 +38,7 @@
| (Const(@{const_name iff},_)$_$_) => th RS @{thm iff_reflection}
| (Const(@{const_name Not},_)$_) => th RS @{thm iff_reflection_F}
| _ => th RS @{thm iff_reflection_T})
- | _ => error ("addsimps: unable to use theorem\n" ^ Display.string_of_thm ctxt th));
+ | _ => error ("addsimps: unable to use theorem\n" ^ Thm.string_of_thm ctxt th));
(*Replace premises x=y, X<->Y by X==Y*)
fun mk_meta_prems ctxt =