Command 'type_synonym' (with single argument) supersedes 'types' (legacy feature);

--- a/NEWS	Fri Dec 17 17:48:05 2010 +0100
+++ b/NEWS	Fri Dec 17 18:10:37 2010 +0100
@@ -83,9 +83,12 @@
 
 *** Pure ***
 
-* Replaced command 'nonterminals' by slightly modernized version
-'nonterminal' (with 'and' separated list of arguments).
-INCOMPATIBILITY.
+* Command 'type_synonym' (with single argument) replaces somewhat
+outdated 'types', which is still available as legacy feature for some
+time.
+
+* Command 'nonterminal' (with 'and' separated list of arguments)
+replaces somewhat outdated 'nonterminals'.  INCOMPATIBILITY.
 
 * Command 'notepad' replaces former 'example_proof' for
 experimentation in Isar without any result.  INCOMPATIBILITY.

--- a/doc-src/IsarRef/Thy/Spec.thy	Fri Dec 17 17:48:05 2010 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy	Fri Dec 17 18:10:37 2010 +0100
@@ -973,13 +973,13 @@
 
 text {*
   \begin{matharray}{rcll}
-    @{command_def "types"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+    @{command_def "type_synonym"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "typedecl"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
   \end{matharray}
 
   \begin{rail}
-    'types' (typespec '=' type mixfix? +)
+    'type_synonym' (typespec '=' type mixfix?)
     ;
     'typedecl' typespec mixfix?
     ;
@@ -989,12 +989,12 @@
 
   \begin{description}
 
-  \item @{command "types"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"} introduces a
-  \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} for the existing type
-  @{text "\<tau>"}.  Unlike actual type definitions, as are available in
-  Isabelle/HOL for example, type synonyms are merely syntactic
-  abbreviations without any logical significance.  Internally, type
-  synonyms are fully expanded.
+  \item @{command "type_synonym"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"}
+  introduces a \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} for the
+  existing type @{text "\<tau>"}.  Unlike actual type definitions, as are
+  available in Isabelle/HOL for example, type synonyms are merely
+  syntactic abbreviations without any logical significance.
+  Internally, type synonyms are fully expanded.
   
   \item @{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} declares a new
   type constructor @{text t}.  If the object-logic defines a base sort

--- a/doc-src/IsarRef/Thy/document/Spec.tex	Fri Dec 17 17:48:05 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Fri Dec 17 18:10:37 2010 +0100
@@ -1010,13 +1010,13 @@
 %
 \begin{isamarkuptext}%
 \begin{matharray}{rcll}
-    \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
+    \indexdef{}{command}{type\_synonym}\hypertarget{command.type-synonym}{\hyperlink{command.type-synonym}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} & (axiomatic!) \\
   \end{matharray}
 
   \begin{rail}
-    'types' (typespec '=' type mixfix? +)
+    'type_synonym' (typespec '=' type mixfix?)
     ;
     'typedecl' typespec mixfix?
     ;
@@ -1026,12 +1026,12 @@
 
   \begin{description}
 
-  \item \hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} introduces a
-  \emph{type synonym} \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} for the existing type
-  \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}}.  Unlike actual type definitions, as are available in
-  Isabelle/HOL for example, type synonyms are merely syntactic
-  abbreviations without any logical significance.  Internally, type
-  synonyms are fully expanded.
+  \item \hyperlink{command.type-synonym}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}}
+  introduces a \emph{type synonym} \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} for the
+  existing type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}}.  Unlike actual type definitions, as are
+  available in Isabelle/HOL for example, type synonyms are merely
+  syntactic abbreviations without any logical significance.
+  Internally, type synonyms are fully expanded.
   
   \item \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} declares a new
   type constructor \isa{t}.  If the object-logic defines a base sort

--- a/etc/isar-keywords-ZF.el	Fri Dec 17 17:48:05 2010 +0100
+++ b/etc/isar-keywords-ZF.el	Fri Dec 17 18:10:37 2010 +0100
@@ -189,6 +189,7 @@
     "txt_raw"
     "typ"
     "type_notation"
+    "type_synonym"
     "typed_print_translation"
     "typedecl"
     "types"
@@ -403,6 +404,7 @@
     "theorems"
     "translations"
     "type_notation"
+    "type_synonym"
     "typed_print_translation"
     "typedecl"
     "types"

--- a/etc/isar-keywords.el	Fri Dec 17 17:48:05 2010 +0100
+++ b/etc/isar-keywords.el	Fri Dec 17 18:10:37 2010 +0100
@@ -250,6 +250,7 @@
     "typ"
     "type_lifting"
     "type_notation"
+    "type_synonym"
     "typed_print_translation"
     "typedecl"
     "typedef"
@@ -516,6 +517,7 @@
     "theorems"
     "translations"
     "type_notation"
+    "type_synonym"
     "typed_print_translation"
     "typedecl"
     "types"

--- a/src/Pure/Isar/isar_syn.ML	Fri Dec 17 17:48:05 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Dec 17 18:10:37 2010 +0100
@@ -111,12 +111,19 @@
     (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
       >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));
 
+val type_abbrev =
+  Parse.type_args -- Parse.binding --
+    (Parse.$$$ "=" |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'));
+
 val _ =
   Outer_Syntax.local_theory "types" "declare type abbreviations" Keyword.thy_decl
-    (Scan.repeat1
-      (Parse.type_args -- Parse.binding --
-        (Parse.$$$ "=" |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix')))
-      >> (fold (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)));
+    (Scan.repeat1 type_abbrev >> (fn specs => fn lthy =>
+     (legacy_feature "Old 'types' commands -- 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));
 
 val _ =
   Outer_Syntax.command "nonterminal"