# HG changeset patch
# User wenzelm
# Date 1318499133 -7200
# Node ID 9b02f6665fc85bde39dceba3016364d27cce0f04
# Parent  2214ba5bdfff1082a7438af526f30f3887c446c4
discontinued obsolete 'types' command;

diff -r 2214ba5bdfff -r 9b02f6665fc8 NEWS
--- a/NEWS	Wed Oct 12 22:48:23 2011 +0200
+++ b/NEWS	Thu Oct 13 11:45:33 2011 +0200
@@ -4,6 +4,12 @@
 New in this Isabelle version
 ----------------------------
 
+*** Pure ***
+
+* Obsolete command 'types' has been discontinued.  Use 'type_synonym'
+instead.  INCOMPATIBILITY.
+
+
 *** HOL ***
 
 * Theory Int: Discontinued many legacy theorems specific to type int.
diff -r 2214ba5bdfff -r 9b02f6665fc8 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Wed Oct 12 22:48:23 2011 +0200
+++ b/etc/isar-keywords-ZF.el	Thu Oct 13 11:45:33 2011 +0200
@@ -190,7 +190,6 @@
     "type_synonym"
     "typed_print_translation"
     "typedecl"
-    "types"
     "ultimately"
     "undo"
     "undos_proof"
@@ -400,7 +399,6 @@
     "type_synonym"
     "typed_print_translation"
     "typedecl"
-    "types"
     "use"))
 
 (defconst isar-keywords-theory-script
diff -r 2214ba5bdfff -r 9b02f6665fc8 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Wed Oct 12 22:48:23 2011 +0200
+++ b/etc/isar-keywords.el	Thu Oct 13 11:45:33 2011 +0200
@@ -264,7 +264,6 @@
     "typed_print_translation"
     "typedecl"
     "typedef"
-    "types"
     "types_code"
     "ultimately"
     "undo"
@@ -539,7 +538,6 @@
     "type_synonym"
     "typed_print_translation"
     "typedecl"
-    "types"
     "types_code"
     "use"))
 
diff -r 2214ba5bdfff -r 9b02f6665fc8 src/HOL/IMP/Fold.thy
--- a/src/HOL/IMP/Fold.thy	Wed Oct 12 22:48:23 2011 +0200
+++ b/src/HOL/IMP/Fold.thy	Thu Oct 13 11:45:33 2011 +0200
@@ -4,7 +4,7 @@
 
 subsection "Simple folding of arithmetic expressions"
 
-types
+type_synonym
   tab = "name \<Rightarrow> val option"
 
 (* maybe better as the composition of substitution and the existing simp_const(0) *)
diff -r 2214ba5bdfff -r 9b02f6665fc8 src/Pure/Isar/isar_syn.ML
--- 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));