# HG changeset patch
# User clasohm
# Date 817660710 -3600
# Node ID f061d2435d63a74d5754acd8f7c7145b02c7492c
# Parent  16330e3fa3b7e19bd28a34870338f442c3a74610
changed syntax diagrams according to quote-less consts and syntax section

diff -r 16330e3fa3b7 -r f061d2435d63 doc-src/Ref/theory-syntax.tex
--- a/doc-src/Ref/theory-syntax.tex	Wed Nov 29 16:56:54 1995 +0100
+++ b/doc-src/Ref/theory-syntax.tex	Wed Nov 29 16:58:30 1995 +0100
@@ -70,8 +70,23 @@
 consts : 'consts' ( ( constDecl ( () | ( '(' mixfix ')' ) ) ) + )
        ;
 
-constDecl : ( name + ',') '::' string ;
+constDecl : ( name + ',') '::' (string | constType) ;
+
+constType : ( applParam * ) applLast;
+
+applParam : ( complexType | '(' paramType ')' |
+              '[' (paramType + ',') ']' ) '=>';
+
+applLast: ( simpleType | '(' (paramType + ',') ')' ) (id *);
 
+complexType: ( simpleType | '(' complexType ')' ) ( id + ) |
+             '(' ( ( complexType | '(' complexType ')' ) + ',' ) ')'
+             id +;
+
+paramType: ( complexType | '(' paramType ')' | '[' ( paramType + ',' ) ']' )
+           ( '=>' paramType * );
+
+simpleType: id | ( tid ( () | '::' id ) );
 
 mixfix :  string ( () | ( () | ('[' (nat + ',') ']')) nat )
        | infix