Pretty.chunks;

--- a/src/Provers/classical.ML	Mon Apr 17 14:08:51 2000 +0200
+++ b/src/Provers/classical.ML	Mon Apr 17 14:10:04 2000 +0200
@@ -270,12 +270,13 @@
 
 fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}) =
   let val pretty_thms = map Display.pretty_thm in
-    Pretty.writeln (Pretty.big_list "safe introduction rules:" (pretty_thms safeIs));
-    Pretty.writeln (Pretty.big_list "unsafe introduction rules:" (pretty_thms hazIs));
-    Pretty.writeln (Pretty.big_list "extra introduction rules:" (pretty_thms xtraIs));
-    Pretty.writeln (Pretty.big_list "safe elimination rules:" (pretty_thms safeEs));
-    Pretty.writeln (Pretty.big_list "unsafe elimination rules:" (pretty_thms hazEs));
-    Pretty.writeln (Pretty.big_list "extra elimination rules:" (pretty_thms xtraEs))
+    [Pretty.big_list "safe introduction rules:" (pretty_thms safeIs),
+      Pretty.big_list "unsafe introduction rules:" (pretty_thms hazIs),
+      Pretty.big_list "extra introduction rules:" (pretty_thms xtraIs),
+      Pretty.big_list "safe elimination rules:" (pretty_thms safeEs),
+      Pretty.big_list "unsafe elimination rules:" (pretty_thms hazEs),
+      Pretty.big_list "extra elimination rules:" (pretty_thms xtraEs)]
+    |> Pretty.chunks |> Pretty.writeln
   end;
 
 fun rep_cs (CS args) = args;

--- a/src/Provers/simplifier.ML	Mon Apr 17 14:08:51 2000 +0200
+++ b/src/Provers/simplifier.ML	Mon Apr 17 14:10:04 2000 +0200
@@ -170,9 +170,10 @@
     fun pretty_proc (name, lhss) =
       Pretty.big_list (name ^ ":") (map Display.pretty_cterm lhss);
   in
-    Pretty.writeln (Pretty.big_list "simplification rules:" (pretty_thms simps));
-    Pretty.writeln (Pretty.big_list "simplification procedures:" (map pretty_proc procs));
-    Pretty.writeln (Pretty.big_list "congruences:" (pretty_thms congs))
+    [Pretty.big_list "simplification rules:" (pretty_thms simps),
+      Pretty.big_list "simplification procedures:" (map pretty_proc procs),
+      Pretty.big_list "congruences:" (pretty_thms congs)]
+    |> Pretty.chunks |> Pretty.writeln
   end;