--- a/src/Pure/Isar/isar_cmd.ML Fri Apr 16 22:15:09 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Fri Apr 16 22:18:59 2010 +0200
@@ -13,7 +13,6 @@
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
@@ -153,11 +152,6 @@
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) =