1.1 --- a/NEWS	Wed Oct 12 22:48:23 2011 +0200
     1.2 +++ b/NEWS	Thu Oct 13 11:45:33 2011 +0200
     1.3 @@ -4,6 +4,12 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** Pure ***
     1.8 +
     1.9 +* Obsolete command 'types' has been discontinued.  Use 'type_synonym'
    1.10 +instead.  INCOMPATIBILITY.
    1.11 +
    1.12 +
    1.13  *** HOL ***
    1.14  
    1.15  * Theory Int: Discontinued many legacy theorems specific to type int.

     2.1 --- a/etc/isar-keywords-ZF.el	Wed Oct 12 22:48:23 2011 +0200
     2.2 +++ b/etc/isar-keywords-ZF.el	Thu Oct 13 11:45:33 2011 +0200
     2.3 @@ -190,7 +190,6 @@
     2.4      "type_synonym"
     2.5      "typed_print_translation"
     2.6      "typedecl"
     2.7 -    "types"
     2.8      "ultimately"
     2.9      "undo"
    2.10      "undos_proof"
    2.11 @@ -400,7 +399,6 @@
    2.12      "type_synonym"
    2.13      "typed_print_translation"
    2.14      "typedecl"
    2.15 -    "types"
    2.16      "use"))
    2.17  
    2.18  (defconst isar-keywords-theory-script

     3.1 --- a/etc/isar-keywords.el	Wed Oct 12 22:48:23 2011 +0200
     3.2 +++ b/etc/isar-keywords.el	Thu Oct 13 11:45:33 2011 +0200
     3.3 @@ -264,7 +264,6 @@
     3.4      "typed_print_translation"
     3.5      "typedecl"
     3.6      "typedef"
     3.7 -    "types"
     3.8      "types_code"
     3.9      "ultimately"
    3.10      "undo"
    3.11 @@ -539,7 +538,6 @@
    3.12      "type_synonym"
    3.13      "typed_print_translation"
    3.14      "typedecl"
    3.15 -    "types"
    3.16      "types_code"
    3.17      "use"))
    3.18  

     4.1 --- a/src/HOL/IMP/Fold.thy	Wed Oct 12 22:48:23 2011 +0200
     4.2 +++ b/src/HOL/IMP/Fold.thy	Thu Oct 13 11:45:33 2011 +0200
     4.3 @@ -4,7 +4,7 @@
     4.4  
     4.5  subsection "Simple folding of arithmetic expressions"
     4.6  
     4.7 -types
     4.8 +type_synonym
     4.9    tab = "name \<Rightarrow> val option"
    4.10  
    4.11  (* maybe better as the composition of substitution and the existing simp_const(0) *)

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