--- 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 *)