# HG changeset patch
# User wenzelm
# Date 1223575402 -7200
# Node ID 86b39d27b199c0fdd0a651072b3c39a163d67c06
# Parent  9b259710d9d3bb47c5213f808c9debdb79fe196b
report: back to single message;

diff -r 9b259710d9d3 -r 86b39d27b199 src/Pure/Isar/outer_keyword.ML
--- a/src/Pure/Isar/outer_keyword.ML	Thu Oct 09 19:24:21 2008 +0200
+++ b/src/Pure/Isar/outer_keyword.ML	Thu Oct 09 20:03:22 2008 +0200
@@ -152,7 +152,7 @@
   let val (keywords, commands) = CRITICAL (fn () =>
     (dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ()))))
   in map report_keyword keywords @ map report_command commands end
-  |> List.app (Output.status o Pretty.string_of);
+  |> Pretty.chunks |> Pretty.string_of |> Output.status;
 
 
 (* augment tables *)