# HG changeset patch
# User clasohm
# Date 815312758 -3600
# Node ID ce35d42d21908aa721af8ffe44ff6f37552c17ac
# Parent  1b731d0b5ad3347d351e791f3173f7c403418e55
extended complex_typ

diff -r 1b731d0b5ad3 -r ce35d42d2190 src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Fri Oct 27 12:21:02 1995 +0100
+++ b/src/HOL/thy_syntax.ML	Thu Nov 02 12:45:58 1995 +0100
@@ -139,17 +139,25 @@
 
   (*parsers*)
   val tvars = type_args >> map (cat "dtVar");
+
+  val simple_typ = ident >> (cat "dtTyp" o curry mk_pair "[]" o quote) ||
+    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";
+    let val typ = simple_typ || "(" $$-- complex_typ --$$ ")";
+        val typ2 = complex_typ || "(" $$-- complex_typ --$$ ")";
+    in
+     (typ -- repeat (ident>>quote) >>
+        (foldl (fn (x,y) => "dtTyp " ^ mk_pair (brackets x, y))) ||
+      "(" $$-- !! (list1 typ2) --$$ ")" -- !! (repeat1 (ident>>quote)) >>
+       (fn (fst, ids) => foldl (fn (x,y) => "dtTyp " ^
+                         mk_pair (brackets x, y)) (commas fst, ids))) toks
+    end;
+
   val opt_typs = repeat (simple_typ || ("(" $$-- complex_typ --$$ ")"));
   val constructor = name -- opt_typs -- opt_mixfix;
 in
   val datatype_decl =
-    (* FIXME tvars -> type_args *)
     tvars -- ident --$$ "=" -- enum1 "|" constructor >> mk_params;
 end;