# HG changeset patch
# User clasohm
# Date 826893279 -3600
# Node ID a82618a900e5d5e08adae920b0fc92babae43e95
# Parent  e3fd931e60958abc226ea939c3868f371b91cc4b
updated syntax of datatype declaration

diff -r e3fd931e6095 -r a82618a900e5 doc-src/Logics/HOL.tex
--- a/doc-src/Logics/HOL.tex	Fri Mar 15 12:01:19 1996 +0100
+++ b/doc-src/Logics/HOL.tex	Fri Mar 15 13:34:39 1996 +0100
@@ -1488,12 +1488,9 @@
 \begin{rail}
 typedecl : typevarlist id '=' (cons + '|')
          ;
-cons     : (id | string) (typ *) ( () | mixfix )
+cons     : name (typ *) ( () | mixfix )
          ;
-typ      : typevarlist id
-           | tid
-         ;
-typevarlist : () | tid | '(' (tid + ',') ')'
+typ      : id | tid | ('(' typevarlist id ')')
          ;
 \end{rail}
 \caption{Syntax of datatype declarations}