# HG changeset patch
# User nipkow
# Date 799484312 -7200
# Node ID 1b30e27aca826552e9d77c580765edb62e3a8348
# Parent  884c6ef06fbfd720a44bfd581bfb2d91dd613349
Simplified layout a little.

diff -r 884c6ef06fbf -r 1b30e27aca82 doc-src/Ref/theory-syntax.tex
--- a/doc-src/Ref/theory-syntax.tex	Wed May 03 08:21:53 1995 +0200
+++ b/doc-src/Ref/theory-syntax.tex	Wed May 03 08:58:32 1995 +0200
@@ -25,7 +25,7 @@
 
 name: id | string;
 
-extension : (section +) 'end' ml;
+extension : (section +) 'end' ( () | ml );
 
 section : classes
         | default
@@ -88,8 +88,7 @@
 defs : 'defs' (( id string ) + )
      ;
 
-ml :  ()
-   | 'ML' text
+ml : 'ML' text
    ;
 
 \end{rail}