1.1 --- a/doc-src/Ref/defining.tex	Fri Jan 27 12:42:03 1995 +0100
     1.2 +++ b/doc-src/Ref/defining.tex	Fri Jan 27 13:29:44 1995 +0100
     1.3 @@ -620,7 +620,7 @@
     1.4  A {\bf binder} is a variable-binding construct such as a quantifier.  The
     1.5  constant declaration
     1.6  \begin{ttbox}
     1.7 -\(c\) :: "\(\sigma\)"   (binder "\(\Q\)" \(pb\) \(p\))
     1.8 +\(c\) :: "\(\sigma\)"   (binder "\(\Q\)" [\(pb\)] \(p\))
     1.9  \end{ttbox}
    1.10  introduces a constant~$c$ of type~$\sigma$, which must have the form
    1.11  $(\tau@1 \To \tau@2) \To \tau@3$.  Its concrete syntax is $\Q~x.P$, where