--- a/src/HOL/thy_syntax.ML Tue Mar 28 12:21:10 1995 +0200
+++ b/src/HOL/thy_syntax.ML Tue Mar 28 12:25:20 1995 +0200
@@ -138,10 +138,12 @@
(*parsers*)
val tvars = type_args >> map (cat "dtVar");
- val typ =
+ val complex_typ =
tvars -- (ident>>quote) >> (cat "dtTyp" o mk_pair o apfst mk_list) ||
type_var >> cat "dtVar";
- val opt_typs = optional ("(" $$-- list1 typ --$$ ")") [];
+ val simple_typ = ident>>(cat "dtTyp" o curry mk_pair "[]" o quote) ||
+ type_var >> cat "dtVar";
+ val opt_typs = repeat (simple_typ || ("(" $$-- complex_typ --$$ ")"));
val constructor = name -- opt_typs -- opt_mixfix;
in
val datatype_decl =