# HG changeset patch
# User wenzelm
# Date 1268487697 -3600
# Node ID d3726291f252d7612e62189ea9375238f8662849
# Parent  35a3b3721ffb9fb17c6c67ea3585da38ffbb3eb6
added typedecl_wrt, which affects default sorts of type args;
misc tuning and simplification;

diff -r 35a3b3721ffb -r d3726291f252 src/Pure/Isar/typedecl.ML
--- a/src/Pure/Isar/typedecl.ML	Sat Mar 13 14:41:14 2010 +0100
+++ b/src/Pure/Isar/typedecl.ML	Sat Mar 13 14:41:37 2010 +0100
@@ -6,6 +6,8 @@
 
 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
 end;
@@ -13,21 +15,24 @@
 structure Typedecl: TYPEDECL =
 struct
 
-fun typedecl (b, vs, mx) lthy =
+fun typedecl_wrt terms (b, vs, 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 = map (fn a => TFree (a, ProofContext.default_sort lthy (a, ~1))) 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 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));
+      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);
   in
@@ -37,16 +42,14 @@
         (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 phi =>
-        let val b' = Morphism.binding phi b
-        in Context.mapping (Sign.type_alias b' name) (ProofContext.type_alias b' name) end)
-    |> ProofContext.type_alias b name
+    |> Local_Theory.type_alias b name
     |> Variable.declare_typ T
     |> pair T
   end;
 
+val typedecl = typedecl_wrt [];
+
 fun typedecl_global decl =
   Theory_Target.init NONE
   #> typedecl decl