--- a/src/Pure/Isar/isar_syn.ML Wed Oct 12 22:48:23 2011 +0200
+++ b/src/Pure/Isar/isar_syn.ML Thu Oct 13 11:45:33 2011 +0200
@@ -118,12 +118,6 @@
(Parse.$$$ "=" |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'));
val _ =
- Outer_Syntax.local_theory "types" "declare type abbreviations" Keyword.thy_decl
- (Scan.repeat1 type_abbrev >> (fn specs => fn lthy =>
- (legacy_feature "Old 'types' command -- use 'type_synonym' instead";
- fold (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs) specs lthy)));
-
-val _ =
Outer_Syntax.local_theory "type_synonym" "declare type abbreviation" Keyword.thy_decl
(type_abbrev >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));