diff -r 60c134fdd290 -r ee19c92ae8b4 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Wed Dec 10 10:44:56 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Wed Dec 10 13:45:44 2014 +0100
@@ -32,7 +32,7 @@
           if Symbol.is_malformed sym
           then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
     val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
-    val reports = Token.report keywords tok :: Token.completion_report tok @ malformed_symbols;
+    val reports = Token.reports keywords tok @ Token.completion_report tok @ malformed_symbols;
   in (is_malformed, reports) end;
 
 in
@@ -44,7 +44,7 @@
 end;
 
 fun present_token keywords tok =
-  Markup.enclose (Token.markup keywords tok) (Output.output (Token.unparse tok));
+  fold_rev Markup.enclose (Token.markups keywords tok) (Output.output (Token.unparse tok));
 
 fun present_span keywords = implode o map (present_token keywords) o Command_Span.content;