--- 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 *)