added nested types on right hand side of datatype definitions
authorclasohm
Fri Sep 08 13:23:04 1995 +0200 (1995-09-08 ago)
changeset 125181fc4d8e3eda
parent 1250 000ecb4fc700
child 1252 27130da22f52
added nested types on right hand side of datatype definitions
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/thy_syntax.ML	Wed Sep 06 15:27:11 1995 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Fri Sep 08 13:23:04 1995 +0200
     1.3 @@ -138,9 +138,10 @@
     1.4  
     1.5    (*parsers*)
     1.6    val tvars = type_args >> map (cat "dtVar");
     1.7 -  val complex_typ =
     1.8 -    tvars -- (ident>>quote) >> (cat "dtTyp" o mk_pair o apfst mk_list) ||
     1.9 -    type_var >> cat "dtVar";
    1.10 +  fun complex_typ toks =
    1.11 +    (("(" $$-- complex_typ  --$$ ")" >> (fn x => [x]) || tvars)
    1.12 +     -- (ident>>quote) >> (cat "dtTyp" o mk_pair o apfst mk_list)
    1.13 +     || type_var >> cat "dtVar") toks;
    1.14    val simple_typ = ident>>(cat "dtTyp" o curry mk_pair "[]" o quote) ||
    1.15      type_var >> cat "dtVar";
    1.16    val opt_typs = repeat (simple_typ || ("(" $$-- complex_typ --$$ ")"));