Improvements wrt rule_tac.

--- a/doc-src/IsarRef/generic.tex	Tue Sep 30 15:07:38 2003 +0200
+++ b/doc-src/IsarRef/generic.tex	Tue Sep 30 15:09:35 2003 +0200
@@ -520,7 +520,8 @@
 
 Note that the tactic emulation proof methods in Isabelle/Isar are consistently
 named $foo_tac$.  Note also that variable names occurring on left hand sides
-of instantiations must be preceded by a question mark if they contain dots.
+of instantiations must be preceded by a question mark if they coincide with
+a keyword or contain dots.
 This is consistent with the attribute $where$ (see \S\ref{sec:pure-meth-att}).
 
 \indexisarmeth{rule-tac}\indexisarmeth{erule-tac}

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

--- a/doc-src/IsarRef/syntax.tex	Tue Sep 30 15:07:38 2003 +0200
+++ b/doc-src/IsarRef/syntax.tex	Tue Sep 30 15:09:35 2003 +0200
@@ -75,9 +75,9 @@
   longident & = & ident\verb,.,ident~\dots~ident \\
   symident & = & sym^+ ~|~ symbol \\
   nat & = & digit^+ \\
-  var & = & \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\
+  var & = & ident ~|~ \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\
   typefree & = & \verb,',ident \\
-  typevar & = & \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\
+  typevar & = & typefree ~|~ \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\
   string & = & \verb,", ~\dots~ \verb,", \\
   verbatim & = & \verb,{*, ~\dots~ \verb,*}, \\
 \end{matharray}