# HG changeset patch
# User wenzelm
# Date 1268949392 -3600
# Node ID 0c71e0d72d7a6ac35136c1f2110a537a3f8da6dd
# Parent  7b7ae5aa396dde63e180cbed80511d54659c3ae3
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
allow sort constraints;
misc tuning and clarification;

diff -r 7b7ae5aa396d -r 0c71e0d72d7a src/Pure/Isar/typedecl.ML
--- a/src/Pure/Isar/typedecl.ML	Tue Mar 16 16:27:28 2010 +0100
+++ b/src/Pure/Isar/typedecl.ML	Thu Mar 18 22:56:32 2010 +0100
@@ -6,50 +6,64 @@
 
 signature TYPEDECL =
 sig
-  val typedecl_wrt: term list -> binding * string list * mixfix ->
-    local_theory -> typ * local_theory
-  val typedecl: binding * string list * mixfix -> local_theory -> typ * local_theory
-  val typedecl_global: binding * string list * mixfix -> theory -> typ * theory
+  val predeclare_constraints: binding * (string * sort) list * mixfix ->
+    local_theory -> string * local_theory
+  val typedecl: binding * (string * sort) list * mixfix -> local_theory -> typ * local_theory
+  val typedecl_global: binding * (string * sort) list * mixfix -> theory -> typ * theory
 end;
 
 structure Typedecl: TYPEDECL =
 struct
 
-fun typedecl_wrt terms (b, vs, mx) lthy =
+(* primitives *)
+
+fun object_logic_arity name thy =
+  (case Object_Logic.get_base_sort thy of
+    NONE => thy
+  | SOME S => AxClass.axiomatize_arity (name, replicate (Sign.arity_number thy name) S, S) thy);
+
+fun basic_typedecl (b, n, mx) lthy =
+  let val name = Local_Theory.full_name lthy b in
+    lthy
+    |> Local_Theory.theory (Sign.add_types [(b, n, NoSyn)] #> object_logic_arity name)
+    |> Local_Theory.type_notation true Syntax.mode_default [(Type (name, replicate n dummyT), mx)]
+    |> Local_Theory.type_alias b name
+    |> pair name
+  end;
+
+
+(* syntactic version -- useful for internalizing additional types/terms beforehand *)
+
+fun predeclare_constraints (b, raw_args, mx) =
+  basic_typedecl (b, length raw_args, mx) ##>
+  fold (Variable.declare_constraints o Logic.mk_type o TFree) raw_args;
+
+
+(* regular version -- without dependencies on type parameters of the context *)
+
+fun typedecl (b, raw_args, mx) lthy =
   let
     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 args_ctxt = lthy |> fold Variable.declare_constraints terms;
-    val args = map (fn a => TFree (a, ProofContext.default_sort args_ctxt (a, ~1))) vs;
-    val T = Type (name, args);
+    val _ = has_duplicates (eq_fst op =) raw_args andalso err "Duplicate parameters";
+    val args = raw_args
+      |> map (fn (a, S) => (a, if S = dummyS then ProofContext.default_sort lthy (a, ~1) else S));
+    val T = Type (Local_Theory.full_name lthy b, map TFree 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 args_ctxt) bad_args));
-
-    val base_sort = Object_Logic.get_base_sort (ProofContext.theory_of lthy);
+        commas_quote (map (Syntax.string_of_typ lthy) bad_args));
   in
     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.type_notation true Syntax.mode_default [(T, mx)]
-    |> Local_Theory.type_alias b name
+    |> basic_typedecl (b, length args, mx)
+    |> snd
     |> Variable.declare_typ T
     |> pair T
   end;
 
-val typedecl = typedecl_wrt [];
-
 fun typedecl_global decl =
   Theory_Target.init NONE
   #> typedecl decl