# HG changeset patch
# User clasohm
# Date 810559384 -7200
# Node ID 81fc4d8e3eda2c2877fb11a69477f80e25eeae20
# Parent  000ecb4fc700fa5f7713a2fa5975b5b106dfd0f9
added nested types on right hand side of datatype definitions

diff -r 000ecb4fc700 -r 81fc4d8e3eda src/HOL/thy_syntax.ML
--- 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 --$$ ")"));