src/Sequents/prover.ML

 
 val empty_pack = Pack([],[]);
 
 fun warn_duplicates [] = []
   | warn_duplicates dups =
-      (warning (cat_lines ("Ignoring duplicate theorems:" :: map Display.string_of_thm dups));
+      (warning (cat_lines ("Ignoring duplicate theorems:" ::
+          map Display.string_of_thm_without_context dups));
        dups);
 
 fun (Pack(safes,unsafes)) add_safes ths   = 
     let val dups = warn_duplicates (gen_inter Thm.eq_thm_prop (ths,safes))
 	val ths' = subtract Thm.eq_thm_prop dups ths

         Pack(sort (make_ord less) (safes@safes'), 
 	     sort (make_ord less) (unsafes@unsafes'));
 
 
 fun print_pack (Pack(safes,unsafes)) =
-    (writeln "Safe rules:";  Display.print_thms safes;
-     writeln "Unsafe rules:"; Display.print_thms unsafes);
+  writeln (cat_lines
+   (["Safe rules:"] @ map Display.string_of_thm_without_context safes @
+    ["Unsafe rules:"] @ map Display.string_of_thm_without_context unsafes));
 
 (*Returns the list of all formulas in the sequent*)
 fun forms_of_seq (Const("SeqO'",_) $ P $ u) = P :: forms_of_seq u
   | forms_of_seq (H $ u) = forms_of_seq u
   | forms_of_seq _ = [];