# HG changeset patch
# User wenzelm
# Date 1268173933 -3600
# Node ID 8b22a498b034a5922c89e8d5c492a80940da3f45
# Parent  8977403824421bbd9d796c95d37bba04ccf11ce5
localized typedecl;

diff -r 897740382442 -r 8b22a498b034 NEWS
--- a/NEWS	Tue Mar 09 23:29:04 2010 +0100
+++ b/NEWS	Tue Mar 09 23:32:13 2010 +0100
@@ -76,6 +76,10 @@
 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.
+
 
 *** HOL ***
 
diff -r 897740382442 -r 8b22a498b034 doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Tue Mar 09 23:29:04 2010 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy	Tue Mar 09 23:32:13 2010 +0100
@@ -954,7 +954,7 @@
 text {*
   \begin{matharray}{rcll}
     @{command_def "types"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{command_def "typedecl"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def "typedecl"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
   \end{matharray}
 
diff -r 897740382442 -r 8b22a498b034 doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Tue Mar 09 23:29:04 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Tue Mar 09 23:32:13 2010 +0100
@@ -991,7 +991,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}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ 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 897740382442 -r 8b22a498b034 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Mar 09 23:29:04 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Mar 09 23:32:13 2010 +0100
@@ -103,16 +103,15 @@
 (* types *)
 
 val _ =
-  OuterSyntax.command "typedecl" "type declaration" K.thy_decl
-    (P.type_args -- P.binding -- P.opt_mixfix >> (fn ((args, a), mx) =>
-      Toplevel.theory (Typedecl.typedecl (a, args, mx) #> snd)));
+  OuterSyntax.local_theory "typedecl" "type declaration" K.thy_decl
+    (P.type_args -- P.binding -- P.opt_mixfix
+      >> (fn ((args, a), mx) => Typedecl.typedecl (a, args, mx) #> snd));
 
 val _ =
   OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
     (Scan.repeat1
       (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_mixfix')))
-      >> (Toplevel.theory o Sign.add_tyabbrs o
-        map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
+      >> (Toplevel.theory o Sign.add_tyabbrs o map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
 
 val _ =
   OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
diff -r 897740382442 -r 8b22a498b034 src/Pure/Isar/typedecl.ML
--- a/src/Pure/Isar/typedecl.ML	Tue Mar 09 23:29:04 2010 +0100
+++ b/src/Pure/Isar/typedecl.ML	Tue Mar 09 23:32:13 2010 +0100
@@ -6,26 +6,50 @@
 
 signature TYPEDECL =
 sig
-  val typedecl: binding * string list * mixfix -> theory -> typ * theory
+  val typedecl: binding * string list * mixfix -> local_theory -> typ * local_theory
+  val typedecl_global: binding * string list * mixfix -> theory -> typ * theory
 end;
 
 structure Typedecl: TYPEDECL =
 struct
 
-fun typedecl (b, vs, mx) thy =
+fun typedecl (b, vs, mx) lthy =
   let
-    val base_sort = Object_Logic.get_base_sort thy;
-    val _ = has_duplicates (op =) vs andalso
-      error ("Duplicate parameters in type declaration " ^ quote (Binding.str_of b));
-    val name = Sign.full_name thy b;
+    fun err msg = error (msg ^ " in type declaration " ^ quote (Binding.str_of b));
+    val _ = has_duplicates (op =) vs andalso err "Duplicate parameters";
+
+    val name = Local_Theory.full_name lthy b;
     val n = length vs;
-    val T = Type (name, map (fn v => TFree (v, [])) vs);
+    val args = map (fn a => TFree (a, ProofContext.default_sort lthy (a, ~1))) vs;
+    val T = Type (name, args);
+
+    val bad_args =
+      #2 (Term.dest_Type (Logic.type_map (singleton (Variable.polymorphic lthy)) T))
+      |> filter_out Term.is_TVar;
+    val _ = not (null bad_args) andalso
+      err ("Locally fixed type arguments " ^ commas_quote (map (Syntax.string_of_typ lthy) bad_args));
+
+    val base_sort = Object_Logic.get_base_sort (ProofContext.theory_of lthy);
   in
-    thy
-    |> Sign.add_types [(b, n, mx)]
-    |> (case base_sort of NONE => I | SOME S => AxClass.axiomatize_arity (name, replicate n S, S))
+    lthy
+    |> Local_Theory.theory
+      (Sign.add_types [(b, n, NoSyn)] #>
+        (case base_sort of
+          NONE => I
+        | SOME S => AxClass.axiomatize_arity (name, replicate n S, S)))
+    |> Local_Theory.checkpoint
+    |> Local_Theory.type_notation true Syntax.mode_default [(T, mx)]
+    |> Local_Theory.type_syntax false
+      (fn _ => Context.mapping (Sign.type_alias b name) (ProofContext.type_alias b name))
+    |> ProofContext.type_alias b name
+    |> Variable.declare_typ T
     |> pair T
   end;
 
+fun typedecl_global decl =
+  Theory_Target.init NONE
+  #> typedecl decl
+  #> Local_Theory.exit_result_global Morphism.typ;
+
 end;