1.1 --- a/doc-src/Ref/introduction.tex	Fri Nov 26 12:54:58 1993 +0100
     1.2 +++ b/doc-src/Ref/introduction.tex	Fri Nov 26 13:00:35 1993 +0100
     1.3 @@ -198,9 +198,10 @@
     1.4  The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$,
     1.5  provided $x$ is not free in ~$f$.  It asserts {\bf extensionality} of
     1.6  functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$.  Higher-order
     1.7 -unification puts terms into a fully $\eta$-expanded form.  For example, if
     1.8 -$F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is $\lambda
     1.9 -h.F(\lambda x.h(x))$.  By default, the user sees this expanded form.
    1.10 +unification occasionally puts terms into a fully $\eta$-expanded form.  For
    1.11 +example, if $F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is
    1.12 +$\lambda h.F(\lambda x.h(x))$.  By default, the user sees this expanded
    1.13 +form.
    1.14  
    1.15  \begin{description}
    1.16  \item[\ttindexbold{eta_contract} \tt:= true;]