--- a/src/HOL/thy_syntax.ML Wed Sep 06 15:27:11 1995 +0200
+++ b/src/HOL/thy_syntax.ML Fri Sep 08 13:23:04 1995 +0200
@@ -138,9 +138,10 @@
(*parsers*)
val tvars = type_args >> map (cat "dtVar");
- val complex_typ =
- tvars -- (ident>>quote) >> (cat "dtTyp" o mk_pair o apfst mk_list) ||
- type_var >> cat "dtVar";
+ fun complex_typ toks =
+ (("(" $$-- complex_typ --$$ ")" >> (fn x => [x]) || tvars)
+ -- (ident>>quote) >> (cat "dtTyp" o mk_pair o apfst mk_list)
+ || type_var >> cat "dtVar") toks;
val simple_typ = ident>>(cat "dtTyp" o curry mk_pair "[]" o quote) ||
type_var >> cat "dtVar";
val opt_typs = repeat (simple_typ || ("(" $$-- complex_typ --$$ ")"));