diff -r 6c7e4d858bae -r 493db7848904 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Apr 17 11:40:00 2008 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Apr 17 16:30:45 2008 +0200
@@ -43,12 +43,12 @@
 (* diagnostics *)
 
 fun report_keyword name =
-  Pretty.markup (Markup.keyword_decl name)
-    [Pretty.str ("Outer syntax keyword: " ^ quote name)];
+  Pretty.mark (Markup.keyword_decl name)
+    (Pretty.str ("Outer syntax keyword: " ^ quote name));
 
 fun report_command name kind =
-  Pretty.markup (Markup.command_decl name kind)
-    [Pretty.str ("Outer syntax command: " ^ quote name ^ " (" ^ kind ^ ")")];
+  Pretty.mark (Markup.command_decl name kind)
+    (Pretty.str ("Outer syntax command: " ^ quote name ^ " (" ^ kind ^ ")"));
 
 
 (* parsers *)