src/Pure/Isar/isar_cmd.ML

   val parse_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
   val parse_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
   val print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
   val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
   val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
+  val add_tyabbrs: (binding * string list * string * mixfix) list -> local_theory -> local_theory
   val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
   val add_axioms: (Attrib.binding * string) list -> theory -> theory
   val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
   val declaration: bool -> Symbol_Pos.text * Position.T -> local_theory -> local_theory
   val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list ->

   |> Context.theory_map;
 
 end;
 
 
+(* old-style type abbreviations *)
+
+val add_tyabbrs = fold (fn (a, args, rhs, mx) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs);
+
+
 (* oracles *)
 
 fun oracle (name, pos) (body_txt, body_pos) =
   let
     val body = Symbol_Pos.content (Symbol_Pos.explode (body_txt, body_pos));