eta_contract: no default;

--- a/doc-src/Ref/introduction.tex	Sat Jul 01 19:55:22 2000 +0200
+++ b/doc-src/Ref/introduction.tex	Sat Jul 01 19:56:46 2000 +0200
@@ -301,7 +301,7 @@
 
 \subsection{Eta-contraction before printing}
 \begin{ttbox} 
-eta_contract: bool ref \hfill{\bf initially false}
+eta_contract: bool ref
 \end{ttbox}
 The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$,
 provided $x$ is not free in ~$f$.  It asserts {\bf extensionality} of