doc-src/Ref/theory-syntax.tex

 
 constType : simpleType | '(' constType ')' | '[' ( constType + "," ) ']'
             '=>' constType | constType '=>' constType;
 
 simpleType: id | ( tid ( () | '::' id ) ) |
-            '(' ( constType + "," ) ')' id | simpleType id;
+            '(' ( constType + "," ) ')' ( id + ',' ) | simpleType ( id + ',' );
 
 mixfix :  string ( () | ( () | ('[' (nat + ',') ']')) nat )
        | infix
        | 'binder' string nat ;