src/Pure/Syntax/syntax.ML

   val type_syn: syntax
   val pure_syn: syntax
   val print_gram: syntax -> unit
   val print_trans: syntax -> unit
   val print_syntax: syntax -> unit
+  val trfun_names: syntax -> string list * string list * string list * string list
   val test_read: syntax -> string -> string -> unit
   val read: syntax -> typ -> string -> term list
   val read_typ: syntax -> ((indexname * sort) list -> indexname -> sort) -> string -> typ
   val simple_read_typ: string -> typ
   val pretty_term: syntax -> bool -> term -> Pretty.T

 (** tables of translation functions **)
 
 (*does not subsume typed print translations*)
 type 'a trtab = (('a list -> 'a) * stamp) Symtab.table;
 
-val dest_trtab = Symtab.dest;
+fun dest_trtab tab = map fst (Symtab.dest tab);
 
 fun lookup_trtab tab c =
   apsome fst (Symtab.lookup (tab, c));
 
 

   extend_syntax ("", true) empty_syntax type_ext;
 
 val pure_syn = extend_syntax ("", true) type_syn pure_ext;
 
 
+
 (** inspect syntax **)
 
 fun pretty_strs_qs name strs =
   Pretty.strs (name :: map quote (sort_strings strs));
 

 (* print_trans *)
 
 fun print_trans (Syntax tabs) =
   let
     fun pretty_trtab name tab =
-      pretty_strs_qs name (map fst (dest_trtab tab));
+      pretty_strs_qs name (dest_trtab tab);
 
     fun pretty_ruletab name tab =
       Pretty.big_list name (map pretty_rule (dest_ruletab tab));
 
     fun pretty_tokentr (mode, trs) = Pretty.strs (quote mode ^ ":" :: map fst trs);

 (* print_syntax *)
 
 fun print_syntax syn = (print_gram syn; print_trans syn);
 
 
+(* trfun_names *)
+
+fun trfun_names (Syntax {parse_ast_trtab, parse_trtab, print_trtab, print_ruletab, ...}) =
+  (dest_trtab parse_ast_trtab, dest_trtab parse_trtab,
+    dest_trtab print_trtab, dest_trtab print_ruletab);
+
+
 
 (** read **)
 
 (* test_read *)