--- 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}