# HG changeset patch
# User wenzelm
# Date 1271449139 -7200
# Node ID 0e5c133b48b663e3bc67d6182c0dbb39a2928bec
# Parent  8e0770d2e49956c0b3c6608d1dbbcdefcabfd62c
keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;

diff -r 8e0770d2e499 -r 0e5c133b48b6 NEWS
--- a/NEWS	Fri Apr 16 22:15:09 2010 +0200
+++ b/NEWS	Fri Apr 16 22:18:59 2010 +0200
@@ -101,9 +101,9 @@
 within a local theory context, with explicit checking of the
 constructors involved (in contrast to the raw 'syntax' versions).
 
-* Command 'typedecl' now works within a local theory context --
-without introducing dependencies on parameters or assumptions, which
-is not possible in Isabelle/Pure.
+* Commands 'types' and 'typedecl' now work within a local theory
+context -- without introducing dependencies on parameters or
+assumptions, which is not possible in Isabelle/Pure.
 
 * Proof terms: Type substitutions on proof constants now use canonical
 order of type variables. INCOMPATIBILITY: Tools working with proof
diff -r 8e0770d2e499 -r 0e5c133b48b6 doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Fri Apr 16 22:15:09 2010 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy	Fri Apr 16 22:18:59 2010 +0200
@@ -953,7 +953,7 @@
 
 text {*
   \begin{matharray}{rcll}
-    @{command_def "types"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def "types"} & : & @{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}
diff -r 8e0770d2e499 -r 0e5c133b48b6 doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Fri Apr 16 22:15:09 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Fri Apr 16 22:18:59 2010 +0200
@@ -990,7 +990,7 @@
 %
 \begin{isamarkuptext}%
 \begin{matharray}{rcll}
-    \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+    \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
     \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
     \indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
   \end{matharray}
diff -r 8e0770d2e499 -r 0e5c133b48b6 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Fri Apr 16 22:15:09 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Apr 16 22:18:59 2010 +0200
@@ -13,7 +13,6 @@
   val print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
   val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
   val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
-  val add_tyabbrs: (binding * string list * string * mixfix) list -> local_theory -> local_theory
   val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
   val add_axioms: (Attrib.binding * string) list -> theory -> theory
   val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
@@ -153,11 +152,6 @@
 end;
 
 
-(* old-style type abbreviations *)
-
-val add_tyabbrs = fold (fn (a, args, rhs, mx) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs);
-
-
 (* oracles *)
 
 fun oracle (name, pos) (body_txt, body_pos) =
diff -r 8e0770d2e499 -r 0e5c133b48b6 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Apr 16 22:15:09 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Apr 16 22:18:59 2010 +0200
@@ -108,15 +108,10 @@
       >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));
 
 val _ =
-  OuterSyntax.local_theory "type_abbrev" "type abbreviation (input only)" K.thy_decl
-    (P.type_args -- P.binding -- P.opt_mixfix -- (P.$$$ "=" |-- P.!!! P.typ)
-      >> (fn (((args, a), mx), rhs) => Typedecl.abbrev_cmd (a, args, mx) rhs #> snd));
-
-val _ =
   OuterSyntax.local_theory "types" "declare type abbreviations" K.thy_decl
     (Scan.repeat1
       (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_mixfix')))
-      >> (IsarCmd.add_tyabbrs o map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
+      >> (fold (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)));
 
 val _ =
   OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"