src/Sequents/simpdata.ML

--- a/src/Sequents/simpdata.ML	Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Sequents/simpdata.ML	Tue Jul 21 01:03:18 2009 +0200
@@ -40,7 +40,7 @@
                     | (Const("Not",_)$_)      => th RS @{thm iff_reflection_F}
                     | _                       => th RS @{thm iff_reflection_T})
            | _ => error ("addsimps: unable to use theorem\n" ^
-                         Display.string_of_thm th));
+                         Display.string_of_thm_without_context th));
 
 (*Replace premises x=y, X<->Y by X==Y*)
 val mk_meta_prems =