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;
authorwenzelm
Fri Apr 16 22:18:59 2010 +0200 (2010-04-16)
changeset 361780e5c133b48b6
parent 36177 8e0770d2e499
child 36179 f45c708bcc01
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;
NEWS
doc-src/IsarRef/Thy/Spec.thy
doc-src/IsarRef/Thy/document/Spec.tex
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
     1.1 --- a/NEWS	Fri Apr 16 22:15:09 2010 +0200
     1.2 +++ b/NEWS	Fri Apr 16 22:18:59 2010 +0200
     1.3 @@ -101,9 +101,9 @@
     1.4  within a local theory context, with explicit checking of the
     1.5  constructors involved (in contrast to the raw 'syntax' versions).
     1.6  
     1.7 -* Command 'typedecl' now works within a local theory context --
     1.8 -without introducing dependencies on parameters or assumptions, which
     1.9 -is not possible in Isabelle/Pure.
    1.10 +* Commands 'types' and 'typedecl' now work within a local theory
    1.11 +context -- without introducing dependencies on parameters or
    1.12 +assumptions, which is not possible in Isabelle/Pure.
    1.13  
    1.14  * Proof terms: Type substitutions on proof constants now use canonical
    1.15  order of type variables. INCOMPATIBILITY: Tools working with proof
     2.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Fri Apr 16 22:15:09 2010 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Fri Apr 16 22:18:59 2010 +0200
     2.3 @@ -953,7 +953,7 @@
     2.4  
     2.5  text {*
     2.6    \begin{matharray}{rcll}
     2.7 -    @{command_def "types"} & : & @{text "theory \<rightarrow> theory"} \\
     2.8 +    @{command_def "types"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     2.9      @{command_def "typedecl"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
    2.10      @{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
    2.11    \end{matharray}
     3.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Fri Apr 16 22:15:09 2010 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Fri Apr 16 22:18:59 2010 +0200
     3.3 @@ -990,7 +990,7 @@
     3.4  %
     3.5  \begin{isamarkuptext}%
     3.6  \begin{matharray}{rcll}
     3.7 -    \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     3.8 +    \indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
     3.9      \indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
    3.10      \indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
    3.11    \end{matharray}
     4.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Apr 16 22:15:09 2010 +0200
     4.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Apr 16 22:18:59 2010 +0200
     4.3 @@ -13,7 +13,6 @@
     4.4    val print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
     4.5    val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
     4.6    val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
     4.7 -  val add_tyabbrs: (binding * string list * string * mixfix) list -> local_theory -> local_theory
     4.8    val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
     4.9    val add_axioms: (Attrib.binding * string) list -> theory -> theory
    4.10    val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
    4.11 @@ -153,11 +152,6 @@
    4.12  end;
    4.13  
    4.14  
    4.15 -(* old-style type abbreviations *)
    4.16 -
    4.17 -val add_tyabbrs = fold (fn (a, args, rhs, mx) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs);
    4.18 -
    4.19 -
    4.20  (* oracles *)
    4.21  
    4.22  fun oracle (name, pos) (body_txt, body_pos) =
     5.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Apr 16 22:15:09 2010 +0200
     5.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Apr 16 22:18:59 2010 +0200
     5.3 @@ -108,15 +108,10 @@
     5.4        >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));
     5.5  
     5.6  val _ =
     5.7 -  OuterSyntax.local_theory "type_abbrev" "type abbreviation (input only)" K.thy_decl
     5.8 -    (P.type_args -- P.binding -- P.opt_mixfix -- (P.$$$ "=" |-- P.!!! P.typ)
     5.9 -      >> (fn (((args, a), mx), rhs) => Typedecl.abbrev_cmd (a, args, mx) rhs #> snd));
    5.10 -
    5.11 -val _ =
    5.12    OuterSyntax.local_theory "types" "declare type abbreviations" K.thy_decl
    5.13      (Scan.repeat1
    5.14        (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_mixfix')))
    5.15 -      >> (IsarCmd.add_tyabbrs o map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
    5.16 +      >> (fold (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)));
    5.17  
    5.18  val _ =
    5.19    OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"