author | wenzelm |
Wed, 24 Sep 2008 19:39:25 +0200 | |
changeset 28345 | 4562584d9d66 |
parent 28344 | f4a17868bde5 |
child 28346 | b8390cd56b8f |
--- a/src/Pure/Isar/outer_keyword.ML Wed Sep 24 19:33:14 2008 +0200 +++ b/src/Pure/Isar/outer_keyword.ML Wed Sep 24 19:39:25 2008 +0200 @@ -148,7 +148,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 - |> Pretty.chunks |> Pretty.string_of |> Output.status; + |> List.app (Output.status o Pretty.string_of); (* augment tables *)