author | wenzelm |
Thu, 09 Oct 2008 20:03:22 +0200 | |
changeset 28542 | 86b39d27b199 |
parent 28541 | 9b259710d9d3 |
child 28543 | 637f2808ab64 |
--- 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 *)