diff -r 2c02c8e212fa -r a67dde8820c0 doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Fri Jul 30 15:59:00 1999 +0200
+++ b/doc-src/IsarRef/syntax.tex	Fri Jul 30 18:27:25 1999 +0200
@@ -35,10 +35,12 @@
 \verb|"let"|).  Already existing objects are usually referenced by
 \railqtoken{nameref}.
 
-\indexoutertoken{name}\indexoutertoken{nameref}
+\indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
 \begin{rail}
   name : ident | symident | string
   ;
+  parname : '(' name ')'
+  ;
   nameref : name | longident
   ;
 \end{rail}