src/Pure/Syntax/syntax_phases.ML

       | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
       | token_trans "_numeral" x = SOME (Pretty.mark_str (Isabelle_Markup.numeral, x))
       | token_trans "_inner_string" x = SOME (Pretty.mark_str (Isabelle_Markup.inner_string, x))
       | token_trans _ _ = NONE;
 
+    fun markup_trans a [Ast.Variable x] = token_trans a x
+      | markup_trans _ _ = NONE;
+
     fun markup_extern c =
       (case Syntax.lookup_const syn c of
         SOME "" => ([], c)
       | SOME b => markup_extern b
       | NONE => c |> Lexicon.unmark

           case_fixed = fn x => free_or_skolem ctxt x,
           case_default = fn x => ([], x)});
   in
     t_to_ast ctxt (Syntax.print_translation syn) t
     |> Ast.normalize ctxt (Syntax.print_rules syn)
-    |> prt_t ctxt (Syntax.prtabs syn) (Syntax.print_ast_translation syn) token_trans markup_extern
+    |> prt_t ctxt (Syntax.prtabs syn) (Syntax.print_ast_translation syn) markup_trans markup_extern
     |> Pretty.markup markup
   end;
 
 in