diff -r bc22daeed49e -r 2a9e918653cc src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sat Jul 07 12:16:18 2007 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sat Jul 07 12:16:19 2007 +0200
@@ -511,19 +511,22 @@
 
 (** pretty terms, typs, sorts **)
 
-fun pretty_t t_to_ast prt_t ctxt (syn as Syntax (tabs, _)) curried t =
+fun pretty_t t_to_ast prt_t markup ctxt (syn as Syntax (tabs, _)) curried t =
   let
     val {print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
     val ast = t_to_ast ctxt (lookup_tr' print_trtab) t;
   in
-    prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
+    Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
       (lookup_tokentr tokentrtab (! print_mode))
-      (Ast.normalize_ast (Symtab.lookup_list print_ruletab) ast)
+      (Ast.normalize_ast (Symtab.lookup_list print_ruletab) ast))
   end;
 
-val pretty_term = pretty_t Printer.term_to_ast o Printer.pretty_term_ast;
-fun pretty_typ ctxt syn = pretty_t Printer.typ_to_ast Printer.pretty_typ_ast ctxt syn false;
-fun pretty_sort ctxt syn = pretty_t Printer.sort_to_ast Printer.pretty_typ_ast ctxt syn false;
+fun pretty_term extern =
+  pretty_t Printer.term_to_ast (Printer.pretty_term_ast extern) Markup.term;
+fun pretty_typ ctxt syn =
+  pretty_t Printer.typ_to_ast Printer.pretty_typ_ast Markup.typ ctxt syn false;
+fun pretty_sort ctxt syn =
+  pretty_t Printer.sort_to_ast Printer.pretty_typ_ast Markup.sort ctxt syn false;