updated syntax of datatype definitions: "C t1 ... tn" instead of "C(t1,...,tn)"

--- a/doc-src/Logics/HOL.tex	Thu Mar 14 12:19:49 1996 +0100
+++ b/doc-src/Logics/HOL.tex	Thu Mar 14 12:21:07 1996 +0100
@@ -1488,7 +1488,7 @@
 \begin{rail}
 typedecl : typevarlist id '=' (cons + '|')
          ;
-cons     : (id | string) ( () | '(' (typ + ',') ')' ) ( () | mixfix )
+cons     : (id | string) (typ *) ( () | mixfix )
          ;
 typ      : typevarlist id
            | tid