diff -r 7286c187596d -r cd05b503ca2d doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Tue Sep 30 15:07:38 2003 +0200
+++ b/doc-src/IsarRef/pure.tex	Tue Sep 30 15:09:35 2003 +0200
@@ -1064,7 +1064,8 @@
 \item [$where~\vec x = \vec t$] performs named instantiation of schematic
   variables occurring in a theorem.  Schematic variables
   have to be specified on the left-hand side (e.g.\ $?x1\!.\!3$).  The
-  question mark may be omitted if the variable name does not contain a dot.
+  question mark may be omitted if the variable name is neither a
+  keyword nor contains a dot.
 
 \end{descr}