tuned signature;

--- a/src/Pure/Syntax/printer.ML	Fri Sep 28 23:45:15 2012 +0200
+++ b/src/Pure/Syntax/printer.ML	Sat Sep 29 13:43:23 2012 +0200
@@ -35,12 +35,12 @@
   val merge_prtabs: prtabs -> prtabs -> prtabs
   val pretty_term_ast: bool -> Proof.context -> prtabs ->
     (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
-    (string -> string -> Pretty.T option) ->
+    (string -> Ast.ast list -> Pretty.T option) ->
     (string -> Markup.T list * string) ->
     Ast.ast -> Pretty.T list
   val pretty_typ_ast: Proof.context -> prtabs ->
     (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
-    (string -> string -> Pretty.T option) ->
+    (string -> Ast.ast list -> Pretty.T option) ->
     (string -> Markup.T list * string) -> Ast.ast -> Pretty.T list
 end;
 
@@ -167,7 +167,7 @@
 
 val pretty_priority = Config.int (Config.declare "Syntax.pretty_priority" (K (Config.Int 0)));
 
-fun pretty type_mode curried ctxt tabs trf token_trans markup_extern ast0 =
+fun pretty type_mode curried ctxt tabs trf markup_trans markup_extern ast0 =
   let
     val show_brackets = Config.get ctxt show_brackets;
 
@@ -188,7 +188,7 @@
             if type_mode then (astT (t, p) @ Ts, args')
             else
               (pretty true curried (Config.put pretty_priority p ctxt)
-                tabs trf token_trans markup_extern t @ Ts, args')
+                tabs trf markup_trans markup_extern t @ Ts, args')
           end
       | synT m (String s :: symbs, args) =
           let
@@ -242,14 +242,11 @@
                 astT (appT (splitT n ([c], args)), p)
               else prnt (prnps, tbs);
       in
-        (case tokentrT a args of
+        (case markup_trans a args of
           SOME prt => [prt]
         | NONE => astT (trf a ctxt args, p) handle Match => prnt ([], tabs))
       end
 
-    and tokentrT a [Ast.Variable x] = token_trans a x
-      | tokentrT _ _ = NONE
-
     and astT (c as Ast.Constant a, p) = combT (c, a, [], p)
       | astT (ast as Ast.Variable _, _) = [Ast.pretty_ast ast]
       | astT (Ast.Appl ((c as Ast.Constant a) :: (args as _ :: _)), p) = combT (c, a, args, p)
@@ -260,14 +257,14 @@
 
 (* pretty_term_ast *)
 
-fun pretty_term_ast curried ctxt prtabs trf tokentrf extern ast =
-  pretty false curried ctxt (mode_tabs prtabs (print_mode_value ())) trf tokentrf extern ast;
+fun pretty_term_ast curried ctxt prtabs trf markup_trans extern ast =
+  pretty false curried ctxt (mode_tabs prtabs (print_mode_value ())) trf markup_trans extern ast;
 
 
 (* pretty_typ_ast *)
 
-fun pretty_typ_ast ctxt prtabs trf tokentrf extern ast =
-  pretty true false ctxt (mode_tabs prtabs (print_mode_value ())) trf tokentrf extern ast;
+fun pretty_typ_ast ctxt prtabs trf markup_trans extern ast =
+  pretty true false ctxt (mode_tabs prtabs (print_mode_value ())) trf markup_trans extern ast;
 
 end;
 

--- a/src/Pure/Syntax/syntax_phases.ML	Fri Sep 28 23:45:15 2012 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sat Sep 29 13:43:23 2012 +0200
@@ -615,6 +615,9 @@
       | 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)
@@ -628,7 +631,7 @@
   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;