support type arguments with sort constraints;

--- a/src/Pure/Isar/outer_parse.ML	Thu Mar 18 23:08:52 2010 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Fri Mar 19 00:41:34 2010 +0100
@@ -68,6 +68,7 @@
   val arity: (string * string list * string) parser
   val multi_arity: (string list * string list * string) parser
   val type_args: string list parser
+  val type_args_constrained: (string * string option) list parser
   val typ_group: string parser
   val typ: string parser
   val mixfix: mixfix parser
@@ -252,11 +253,14 @@
 
 val typ = inner_syntax typ_group;
 
-val type_args =
-  type_ident >> single ||
-  $$$ "(" |-- !!! (list1 type_ident --| $$$ ")") ||
+fun type_arguments arg =
+  arg >> single ||
+  $$$ "(" |-- !!! (list1 arg --| $$$ ")") ||
   Scan.succeed [];
 
+val type_args = type_arguments type_ident;
+val type_args_constrained = type_arguments (type_ident -- Scan.option ($$$ "::" |-- !!! sort));
+
 
 (* mixfix annotations *)
 

--- a/src/Pure/Isar/typedecl.ML	Thu Mar 18 23:08:52 2010 +0100
+++ b/src/Pure/Isar/typedecl.ML	Fri Mar 19 00:41:34 2010 +0100
@@ -6,6 +6,7 @@
 
 signature TYPEDECL =
 sig
+  val read_constraint: Proof.context -> string option -> sort
   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
@@ -34,6 +35,9 @@
 
 (* syntactic version -- useful for internalizing additional types/terms beforehand *)
 
+fun read_constraint _ NONE = dummyS
+  | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
+
 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;