diff -r f3a8476285c6 -r f231a7594e54 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sat Jun 25 17:17:49 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sat Jun 25 18:15:36 2011 +0200
@@ -624,7 +624,7 @@
         SOME "" => ([], c)
       | SOME b => markup_extern b
       | NONE => c |> Lexicon.unmark
-         {case_class = fn x => ([Markup.tclass x], Proof_Context.extern_class ctxt x),
+         {case_class = fn x => (markup_class ctxt x, Proof_Context.extern_class ctxt x),
           case_type = fn x => ([Markup.tycon x], Proof_Context.extern_type ctxt x),
           case_const = fn x => ([Markup.const x], Proof_Context.extern_const ctxt x),
           case_fixed = fn x => free_or_skolem ctxt x,