# HG changeset patch
# User wenzelm
# Date 933601230 -7200
# Node ID d203e2282789567f6b8614b22a7a36b8b96b8cf0
# Parent  d0c2168f77041eff6056062318b359feee4ef27f
cat_lines;

diff -r d0c2168f7704 -r d203e2282789 src/Sequents/prover.ML
--- a/src/Sequents/prover.ML	Mon Aug 02 15:39:23 1999 +0200
+++ b/src/Sequents/prover.ML	Mon Aug 02 15:40:30 1999 +0200
@@ -28,8 +28,7 @@
 
 fun warn_duplicates [] = []
   | warn_duplicates dups =
-      (warning (String.concat ("Ignoring duplicate theorems:\n"::
-			       map (suffix "\n" o string_of_thm) dups));
+      (warning (cat_lines ("Ignoring duplicate theorems:" :: map string_of_thm dups));
        dups);
 
 fun (Pack(safes,unsafes)) add_safes ths   =