src/Sequents/simpdata.ML

--- a/src/Sequents/simpdata.ML	Fri May 16 23:25:37 2008 +0200
+++ b/src/Sequents/simpdata.ML	Sat May 17 13:54:30 2008 +0200
@@ -126,7 +126,7 @@
                     | (Const("Not",_)$_)      => th RS iff_reflection_F
                     | _                       => th RS iff_reflection_T)
            | _ => error ("addsimps: unable to use theorem\n" ^
-                         string_of_thm th));
+                         Display.string_of_thm th));
 
 (*Replace premises x=y, X<->Y by X==Y*)
 val mk_meta_prems =