--- a/src/Pure/Thy/thy_parse.ML Wed Nov 29 16:44:59 1995 +0100
+++ b/src/Pure/Thy/thy_parse.ML Wed Nov 29 16:47:38 1995 +0100
@@ -259,7 +259,9 @@
(* consts *)
-val simple_type = ident || kind TypeVar;
+val simple_type = ident ||
+ (kind TypeVar -- optional ("::" $$-- ident >> cat "::") "" >>
+ (fn (tv, cl) => tv ^ cl));
(*Types with type arguments, like e.g. "'a list list"*)
fun complex_type toks =
@@ -274,7 +276,7 @@
(*Const type which is limited at the end by "=>", ")", "]" or ","*)
fun param_type toks =
((complex_type || "(" $$-- param_type --$$ ")" >> parens ||
- "[" $$-- !! (list1 param_type) --$$ "]" >> mk_list) --
+ "[" $$-- (list1 param_type) --$$ "]" >> mk_list) --
repeat ("=>" $$-- param_type >> cat " =>") >>
(fn (t, ts) => t ^ implode ts)) toks;