Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Sequents/prover.ML
changeset 26928 ca87aff1ad2d
parent 22360 26ead7ed4f4b
child 29269 5c25a2012975 
--- 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
isabelle