1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Oct 26 12:19:01 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Oct 26 12:19:01 2010 +0200
     1.3 @@ -401,12 +401,10 @@
     1.4    \begin{rail}
     1.5      'primrec' target? fixes 'where' equations
     1.6      ;
     1.7 +    ('fun' | 'function') target? functionopts? fixes \\ 'where' equations
     1.8 +    ;
     1.9      equations: (thmdecl? prop + '|')
    1.10      ;
    1.11 -    ('fun' | 'function') target? functionopts? fixes 'where' clauses
    1.12 -    ;
    1.13 -    clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|')
    1.14 -    ;
    1.15      functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')'
    1.16      ;
    1.17      'termination' ( term )?

     2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Oct 26 12:19:01 2010 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Oct 26 12:19:01 2010 +0200
     2.3 @@ -411,12 +411,10 @@
     2.4    \begin{rail}
     2.5      'primrec' target? fixes 'where' equations
     2.6      ;
     2.7 +    ('fun' | 'function') target? functionopts? fixes \\ 'where' equations
     2.8 +    ;
     2.9      equations: (thmdecl? prop + '|')
    2.10      ;
    2.11 -    ('fun' | 'function') target? functionopts? fixes 'where' clauses
    2.12 -    ;
    2.13 -    clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|')
    2.14 -    ;
    2.15      functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')'
    2.16      ;
    2.17      'termination' ( term )?