changed syntax of datatype declarations (curried types for constructor
parameters)

--- a/src/HOL/IMP/Com.thy	Tue Mar 28 12:21:10 1995 +0200
+++ b/src/HOL/IMP/Com.thy	Tue Mar 28 12:25:20 1995 +0200
@@ -19,10 +19,10 @@
 arities loc :: term
 
 datatype
-  aexp = N (nat)
-       | X (loc)
-       | Op1 (n2n, aexp)
-       | Op2 (n2n2n, aexp, aexp)
+  aexp = N nat
+       | X loc
+       | Op1 n2n aexp
+       | Op2 n2n2n aexp aexp
 
 (** Evaluation of arithmetic expressions **)
 consts  evala    :: "(aexp*state*nat)set"
@@ -44,10 +44,10 @@
 datatype
   bexp = true
        | false
-       | ROp  (n2n2b, aexp, aexp)
-       | noti (bexp)
-       | andi (bexp,bexp)	(infixl 60)
-       | ori  (bexp,bexp)	(infixl 60)
+       | ROp  n2n2b aexp aexp
+       | noti bexp
+       | andi bexp bexp 	(infixl 60)
+       | ori  bexp bexp 	(infixl 60)
 
 (** Evaluation of boolean expressions **)
 consts evalb	:: "(bexp*state*bool)set"	
@@ -72,10 +72,10 @@
 
 datatype
   com = skip
-      | ":="   (loc,aexp)	 (infixl  60)
-      | semic  (com,com)	 ("_; _"  [60, 60] 10)
-      | whileC (bexp,com)	 ("while _ do _"  60)
-      | ifC    (bexp, com, com)	 ("ifc _ then _ else _"  60)
+      | ":="   loc aexp	         (infixl  60)
+      | semic  com com	         ("_; _"  [60, 60] 10)
+      | whileC bexp com	         ("while _ do _"  60)
+      | ifC    bexp com com	 ("ifc _ then _ else _"  60)
 
 (** Execution of commands **)
 consts  evalc    :: "(com*state*state)set"

--- a/src/HOL/List.thy	Tue Mar 28 12:21:10 1995 +0200
+++ b/src/HOL/List.thy	Tue Mar 28 12:25:20 1995 +0200
@@ -9,7 +9,7 @@
 
 List = Arith +
 
-datatype 'a list = "[]" ("[]") | "#"('a,'a list) (infixr 65)
+datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65)
 
 consts
 

--- a/src/HOL/ex/PropLog.thy	Tue Mar 28 12:21:10 1995 +0200
+++ b/src/HOL/ex/PropLog.thy	Tue Mar 28 12:25:20 1995 +0200
@@ -8,7 +8,7 @@
 
 PropLog = Finite +
 datatype
-    'a pl = false | var ('a) ("#_" [1000]) | "->" ('a pl,'a pl) (infixr 90)
+    'a pl = false | var 'a ("#_" [1000]) | "->" ('a pl) ('a pl) (infixr 90)
 consts
   thms :: "'a pl set => 'a pl set"
   "|-" 	:: "['a pl set, 'a pl] => bool"	(infixl 50)

--- a/src/HOL/ex/String.thy	Tue Mar 28 12:21:10 1995 +0200
+++ b/src/HOL/ex/String.thy	Tue Mar 28 12:25:20 1995 +0200
@@ -11,7 +11,7 @@
          | H08 | H09 | H0A | H0B | H0C | H0D | H0E | H0F
 
 datatype
-  char = Char (nibble, nibble)
+  char = Char nibble nibble
 
 types
   string = "char list"

--- 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 =