# HG changeset patch
# User wenzelm
# Date 791209784 -3600
# Node ID 190f89d8563c06469b334cbe5be0590be395101e
# Parent  35c836adf48fa45f34cf1e1b3aa910f937e9d7f2
binder: optional body pri now [bracketted];

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