diff -r bdb88b1cb2b7 -r c539d3c9c023 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 15:43:45 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Apr 06 16:15:57 2011 +0200
@@ -89,8 +89,6 @@
 
 (* parsetree_to_ast *)
 
-fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c);
-
 fun parsetree_to_ast ctxt constrain_pos trf parsetree =
   let
     val tsig = ProofContext.tsig_of ctxt;
@@ -240,7 +238,7 @@
 fun parse_asts ctxt raw root (syms, pos) =
   let
     val syn = ProofContext.syn_of ctxt;
-    val {parse_ast_trtab, ...} = Syntax.rep_syntax syn;
+    val ast_tr = Syntax.parse_ast_translation syn;
 
     val toks = Syntax.tokenize syn raw syms;
     val _ = List.app (Lexicon.report_token ctxt) toks;
@@ -263,14 +261,16 @@
             map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))));
 
     val constrain_pos = not raw andalso Config.get ctxt Syntax.positions;
-    val parsetree_to_ast = parsetree_to_ast ctxt constrain_pos (lookup_tr parse_ast_trtab);
+    val parsetree_to_ast = parsetree_to_ast ctxt constrain_pos ast_tr;
   in map parsetree_to_ast pts end;
 
 fun parse_raw ctxt root input =
   let
-    val {parse_ruletab, parse_trtab, ...} = Syntax.rep_syntax (ProofContext.syn_of ctxt);
+    val syn = ProofContext.syn_of ctxt;
+    val tr = Syntax.parse_translation syn;
+    val {parse_ruletab, ...} = Syntax.rep_syntax syn;
     val norm = Ast.normalize ctxt (Symtab.lookup_list parse_ruletab);
-    val ast_to_term = ast_to_term ctxt (lookup_tr parse_trtab);
+    val ast_to_term = ast_to_term ctxt tr;
   in
     parse_asts ctxt false root input
     |> (map o apsnd o Exn.maps_result) (norm #> Exn.interruptible_capture ast_to_term)
@@ -558,17 +558,18 @@
 
 local
 
-fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c);
-
 fun unparse_t t_to_ast prt_t markup ctxt curried t =
   let
-    val {print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} =
-      Syntax.rep_syntax (ProofContext.syn_of ctxt);
-    val ast = t_to_ast ctxt (lookup_tr' print_trtab) t;
+    val syn = ProofContext.syn_of ctxt;
+    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;
   in
-    Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
-      (Syntax.lookup_tokentr tokentrtab (print_mode_value ()))
-      (Ast.normalize ctxt (Symtab.lookup_list print_ruletab) ast))
+    t_to_ast ctxt tr' t
+    |> Ast.normalize ctxt (Symtab.lookup_list print_ruletab)
+    |> prt_t ctxt curried prtabs ast_tr' tokentr
+    |> Pretty.markup markup
   end;
 
 in