diff -r 47aa9df578ea -r 8263d0b50e12 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Wed Aug 04 18:20:05 1999 +0200
+++ b/doc-src/IsarRef/generic.tex	Wed Aug 04 18:20:24 1999 +0200
@@ -53,13 +53,19 @@
 \begin{rail}
   ('tag' | 'untag') (nameref+)
   ;
+\end{rail}
+
+\begin{rail}
   ('COMP' | 'RS') nat? thmref
   ;
   'OF' thmrefs
   ;
-  'where' (term '=' term * 'and')
+\end{rail}
+
+\begin{rail}
+  'where' (name '=' term * 'and')
   ;
-  'of' (inst * ) ('concl:' (inst * ))?
+  'of' (inst * ) ('concl' ':' (inst * ))?
   ;
 
   inst: underscore | term