--- a/src/Sequents/prover.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Sequents/prover.ML Tue Jul 21 01:03:18 2009 +0200
@@ -27,7 +27,8 @@
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 =
@@ -50,8 +51,9 @@
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