# HG changeset patch
# User clasohm
# Date 817824009 -3600
# Node ID 63c3d78df538bfa50c31d8d2902e1f4f46374ed1
# Parent  007ad29ce6cacaaedbf7067fca549ca3ab2c8c84
changed typeDecl

diff -r 007ad29ce6ca -r 63c3d78df538 doc-src/Ref/theory-syntax.tex
--- a/doc-src/Ref/theory-syntax.tex	Fri Dec 01 14:17:50 1995 +0100
+++ b/doc-src/Ref/theory-syntax.tex	Fri Dec 01 14:20:09 1995 +0100
@@ -53,7 +53,14 @@
 types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + )
       ;
 
-typeDecl : ( () | tid | '(' ( tid + ',' ) ')') name ( () | '='  string );
+typeDecl : ( () | tid | '(' ( tid + ',' ) ')') name
+           ( () | '=' ( string | type ) );
+
+type : simpleType | '(' type ')' | type '=>' type |
+       '[' ( type + "," ) ']' '=>' type;
+
+simpleType: id | ( tid ( () | '::' id ) ) |
+            '(' ( type + "," ) ')' id | simpleType id;
 
 infix : ( 'infixr' | 'infixl' ) nat;
 
@@ -72,12 +79,6 @@
 
 constDecl : ( name + ',') '::' (string | type);
 
-type : simpleType | '(' type ')' | type '=>' type |
-       '[' ( type + "," ) ']' '=>' type;
-
-simpleType: id | ( tid ( () | '::' id ) ) |
-            '(' ( type + "," ) ')' id | simpleType id;
-
 mixfix :  string ( () | ( () | ('[' (nat + ',') ']')) nat )
        | infix
        | 'binder' string nat ;