--- 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.
--- 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
--- 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"))
--- 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) *)
--- 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));