diff -r 222810ce6b05 -r 6588b947d631 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Wed Nov 29 23:33:09 2006 +0100
+++ b/doc-src/IsarRef/generic.tex	Thu Nov 30 14:17:22 2006 +0100
@@ -23,19 +23,21 @@
 available, and result names need not be given.
 
 \begin{rail}
-  'axiomatization' target? consts? ('where' specs)?
+  'axiomatization' target? fixes? ('where' specs)?
   ;
-  'definition' target? (constdecl? constdef +)
+  'definition' target? (decl 'where')? thmdecl? prop
   ;
-  'abbreviation' target? mode? (constdecl? prop +)
+  'abbreviation' target? mode? (decl 'where')? prop
   ;
   'notation' target? mode? (nameref mixfix + 'and')
   ;
 
-  consts: ((name ('::' type)? structmixfix? | vars) + 'and')
+  fixes: ((name ('::' type)? mixfix? | vars) + 'and')
   ;
   specs: (thmdecl? props + 'and')
   ;
+  decl: name ('::' type)? mixfix?
+  ;
 \end{rail}
 
 \begin{descr}