1.1 --- a/doc-src/IsarRef/pure.tex	Sat Apr 09 15:34:38 2005 +0200
     1.2 +++ b/doc-src/IsarRef/pure.tex	Sat Apr 09 15:35:37 2005 +0200
     1.3 @@ -1038,7 +1038,7 @@
     1.4    ;
     1.5    'of' insts ('concl' ':' insts)?
     1.6    ;
     1.7 -  'where' (name '=' term * 'and')
     1.8 +  'where' ((name | var | typefree | typevar) '=' (type | term) * 'and')
     1.9    ;
    1.10  \end{rail}
    1.11  
    1.12 @@ -1099,21 +1099,18 @@
    1.13    \cite[\S5]{isabelle-ref}, but note the reversed order.  Positions may be
    1.14    effectively skipped by including ``$\_$'' (underscore) as argument.
    1.15    
    1.16 -\item [$of~\vec t$] performs positional instantiation of term
    1.17 -  variables.  The terms $\vec t$ are substituted for any schematic
    1.18 -  variables occurring in a theorem from left to right; ``\texttt{_}''
    1.19 -  (underscore) indicates to skip a position.  Arguments following a
    1.20 -  ``$concl\colon$'' specification refer to positions of the conclusion
    1.21 -  of a rule.
    1.22 +\item [$of~\vec t$] performs positional instantiation of term variables.  The
    1.23 +  terms $\vec t$ are substituted for any schematic variables occurring in a
    1.24 +  theorem from left to right; ``\texttt{_}'' (underscore) indicates to skip a
    1.25 +  position.  Arguments following a ``$concl\colon$'' specification refer to
    1.26 +  positions of the conclusion of a rule.
    1.27    
    1.28 -\item [$where~\vec x = \vec t$] performs named instantiation of
    1.29 -  schematic type and term variables occurring in a theorem.  Schematic
    1.30 -  variables have to be specified on the left-hand side (e.g.\
    1.31 -  $?x1\!.\!3$).  The question mark may be omitted if the variable name
    1.32 -  is neither a keyword nor contains a dot.  Types are instantiated
    1.33 -  before terms, and instantiations have to be written in that order.
    1.34 -  Because type instantiations are inferred from term instantiations,
    1.35 -  explicit type instantiations are seldom necessary.
    1.36 +\item [$where~\vec x = \vec t$] performs named instantiation of schematic type
    1.37 +  and term variables occurring in a theorem.  Schematic variables have to be
    1.38 +  specified on the left-hand side (e.g.\ $?x1\!.\!3$).  The question mark may
    1.39 +  be omitted if the variable name is a plain identifier without index.  As
    1.40 +  type instantiations are inferred from term instantiations, explicit type
    1.41 +  instantiations are seldom necessary.
    1.42  
    1.43  \end{descr}
    1.44