diff -r 8684b5240f11 -r ca87aff1ad2d src/Sequents/prover.ML
--- a/src/Sequents/prover.ML	Fri May 16 23:25:37 2008 +0200
+++ b/src/Sequents/prover.ML	Sat May 17 13:54:30 2008 +0200
@@ -28,7 +28,7 @@
 
 fun warn_duplicates [] = []
   | warn_duplicates dups =
-      (warning (cat_lines ("Ignoring duplicate theorems:" :: map string_of_thm dups));
+      (warning (cat_lines ("Ignoring duplicate theorems:" :: map Display.string_of_thm dups));
        dups);
 
 fun (Pack(safes,unsafes)) add_safes ths   = 
@@ -51,8 +51,8 @@
 
 
 fun print_pack (Pack(safes,unsafes)) =
-    (writeln "Safe rules:";  print_thms safes;
-     writeln "Unsafe rules:"; print_thms unsafes);
+    (writeln "Safe rules:";  Display.print_thms safes;
+     writeln "Unsafe rules:"; Display.print_thms unsafes);
 
 (*Returns the list of all formulas in the sequent*)
 fun forms_of_seq (Const("SeqO'",_) $ P $ u) = P :: forms_of_seq u