more abstract print translation;

--- a/src/Pure/Syntax/printer.ML	Wed Apr 06 16:15:57 2011 +0200
+++ b/src/Pure/Syntax/printer.ML	Wed Apr 06 17:00:40 2011 +0200
@@ -23,7 +23,6 @@
   val show_question_marks_raw: Config.raw
   val show_question_marks: bool Config.T
   val pretty_priority: int Config.T
-  val apply_trans: 'a -> ('a -> 'b -> 'c) list -> 'b -> 'c
 end;
 
 signature PRINTER =
@@ -36,11 +35,11 @@
   val merge_prtabs: prtabs -> prtabs -> prtabs
   val pretty_term_ast: {extern_class: string -> xstring, extern_type: string -> xstring,
       extern_const: string -> xstring} -> Proof.context -> bool -> prtabs ->
-    (string -> (Proof.context -> Ast.ast list -> Ast.ast) list) ->
+    (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
     (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
   val pretty_typ_ast: {extern_class: string -> xstring, extern_type: string -> xstring} ->
     Proof.context -> bool -> prtabs ->
-    (string -> (Proof.context -> Ast.ast list -> Ast.ast) list) ->
+    (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
     (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
 end;
 
@@ -161,12 +160,6 @@
 
 (** pretty term or typ asts **)
 
-fun apply_trans ctxt fns args =
-  let
-    fun app_first [] = raise Match
-      | app_first (f :: fs) = f ctxt args handle Match => app_first fs;
-  in app_first fns end;
-
 fun is_chain [Block (_, pr)] = is_chain pr
   | is_chain [Arg _] = true
   | is_chain _  = false;
@@ -264,7 +257,7 @@
       in
         (case tokentrT a args of
           SOME prt => [prt]
-        | NONE => astT (apply_trans ctxt (trf a) args, p) handle Match => prnt ([], tabs))
+        | NONE => astT (trf a ctxt args, p) handle Match => prnt ([], tabs))
       end
 
     and tokentrT a [Ast.Variable x] = token_trans a x

--- a/src/Pure/Syntax/syntax.ML	Wed Apr 06 16:15:57 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Wed Apr 06 17:00:40 2011 +0200
@@ -120,8 +120,10 @@
   val parse: Proof.context -> syntax -> string -> Lexicon.token list -> Parser.parsetree list
   val parse_ast_translation: syntax -> string -> (Proof.context -> Ast.ast list -> Ast.ast) option
   val parse_translation: syntax -> string -> (Proof.context -> term list -> term) option
-  val print_translation: syntax -> string -> (Proof.context -> typ -> term list -> term) list
-  val print_ast_translation: syntax -> string -> (Proof.context -> Ast.ast list -> Ast.ast) list
+  val print_translation: syntax -> string ->
+    Proof.context -> typ -> term list -> term  (*exception Match*)
+  val print_ast_translation: syntax -> string ->
+    Proof.context -> Ast.ast list -> Ast.ast  (*exception Match*)
   val token_translation: syntax -> string list ->
     string -> (Proof.context -> string -> Pretty.T) option
   type mode
@@ -421,7 +423,19 @@
 
 (* print (ast) translations *)
 
-fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c);
+fun apply_tr' tab c ctxt T args =
+  let
+    val fns = map fst (Symtab.lookup_list tab c);
+    fun app_first [] = raise Match
+      | app_first (f :: fs) = f ctxt T args handle Match => app_first fs;
+  in app_first fns end;
+
+fun apply_ast_tr' tab c ctxt args =
+  let
+    val fns = map fst (Symtab.lookup_list tab c);
+    fun app_first [] = raise Match
+      | app_first (f :: fs) = f ctxt args handle Match => app_first fs;
+  in app_first fns end;
 
 fun update_tr'tab trfuns = fold_rev (Symtab.update_list Syn_Ext.eq_trfun) trfuns;
 fun remove_tr'tab trfuns = fold (Symtab.remove_list Syn_Ext.eq_trfun) trfuns;
@@ -507,8 +521,8 @@
 
 fun parse_ast_translation (Syntax ({parse_ast_trtab, ...}, _)) = lookup_tr parse_ast_trtab;
 fun parse_translation (Syntax ({parse_trtab, ...}, _)) = lookup_tr parse_trtab;
-fun print_translation (Syntax ({print_trtab, ...}, _)) = lookup_tr' print_trtab;
-fun print_ast_translation (Syntax ({print_ast_trtab, ...}, _)) = lookup_tr' print_ast_trtab;
+fun print_translation (Syntax ({print_trtab, ...}, _)) = apply_tr' print_trtab;
+fun print_ast_translation (Syntax ({print_ast_trtab, ...}, _)) = apply_ast_tr' print_ast_trtab;
 fun token_translation (Syntax ({tokentrtab, ...}, _)) = lookup_tokentr tokentrtab;
 
 type mode = string * bool;

--- a/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 16:15:57 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 17:00:40 2011 +0200
@@ -443,8 +443,6 @@
 
 (* sort_to_ast and typ_to_ast *)
 
-fun apply_typed x fs = map (fn f => fn ctxt => f ctxt x) fs;
-
 fun ast_of_termT ctxt trf tm =
   let
     val ctxt' = Config.put show_sorts false ctxt;
@@ -456,9 +454,8 @@
             (Const (a, _), args) => trans a args
           | (f, args) => Ast.Appl (map ast_of (f :: args)))
       | ast_of t = simple_ast_of ctxt t
-    and trans a args =
-      ast_of (Syntax.apply_trans ctxt' (apply_typed dummyT (trf a)) args)
-        handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
+    and trans a args = ast_of (trf a ctxt' dummyT args)
+      handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
   in ast_of tm end;
 
 fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (term_of_sort S);
@@ -535,9 +532,8 @@
           else trans c T ts
       | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
 
-    and trans a T args =
-      ast_of (Syntax.apply_trans ctxt (apply_typed T (trf a)) args)
-        handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
+    and trans a T args = ast_of (trf a ctxt T args)
+      handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
 
     and constrain t T =
       if show_types andalso T <> dummyT then
@@ -564,7 +560,7 @@
     val tr' = Syntax.print_translation syn;
     val ast_tr' = Syntax.print_ast_translation syn;
     val tokentr = Syntax.token_translation syn (print_mode_value ());
-    val {print_ruletab, tokentrtab, prtabs, ...} = Syntax.rep_syntax syn;
+    val {print_ruletab, prtabs, ...} = Syntax.rep_syntax syn;
   in
     t_to_ast ctxt tr' t
     |> Ast.normalize ctxt (Symtab.lookup_list print_ruletab)