# 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 =