src/Provers/simplifier.ML

 
     val pretty_thms = map Display.pretty_thm;
     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;
 
 
 (* extend simpsets *)