src/Pure/Isar/isar_cmd.ML

   val parse_ast_translation: bool * (string * Position.T) -> theory -> theory
   val parse_translation: bool * (string * Position.T) -> theory -> theory
   val print_translation: bool * (string * Position.T) -> theory -> theory
   val typed_print_translation: bool * (string * Position.T) -> theory -> theory
   val print_ast_translation: bool * (string * Position.T) -> theory -> theory
-  val token_translation: string * Position.T -> theory -> theory
   val oracle: bstring -> string -> string * Position.T -> theory -> theory
   val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
   val add_defs: (bool * bool) * ((bstring * string) * Attrib.src list) list -> theory -> theory
   val apply_theorems: (Facts.ref * Attrib.src list) list -> theory -> thm list * theory
   val apply_theorems_i: (thm list * attribute list) list -> theory -> thm list * theory

     ("val typed_print_translation: (string * (" ^ advancedT a ^
       "bool -> typ -> term list -> term)) list")
     ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)")
   |> Context.theory_map;
 
-fun token_translation (txt, pos) =
-  txt |> ML_Context.expression pos
-    "val token_translation: (string * string * (Proof.context -> string -> Pretty.T)) list"
-      "Context.map_theory (Sign.add_tokentrfuns token_translation)"
-  |> Context.theory_map;
-
 end;
 
 
 (* oracles *)