diff -r 8cdddd689ea9 -r a4b2bb0dab08 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Sun May 30 14:14:30 2010 +0200
+++ b/src/Pure/General/pretty.ML	Sun May 30 14:21:35 2010 +0200
@@ -137,8 +137,8 @@
 
 fun markup m prts = markup_block m (0, prts);
 fun mark m prt = markup m [prt];
-fun keyword name = mark (Markup.keyword name) (str name);
-fun command name = mark (Markup.command name) (str name);
+fun keyword name = mark Markup.keyword (str name);
+fun command name = mark Markup.command (str name);
 
 fun markup_chunks m prts = markup m (fbreaks prts);
 val chunks = markup_chunks Markup.none;