diff -r 11ea439d947f -r 751121d5ca35 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Oct 26 12:19:01 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Oct 26 12:19:01 2010 +0200
@@ -401,11 +401,9 @@
   \begin{rail}
     'primrec' target? fixes 'where' equations
     ;
-    equations: (thmdecl? prop + '|')
+    ('fun' | 'function') target? functionopts? fixes \\ 'where' equations
     ;
-    ('fun' | 'function') target? functionopts? fixes 'where' clauses
-    ;
-    clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|')
+    equations: (thmdecl? prop + '|')
     ;
     functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')'
     ;