# HG changeset patch
# User clasohm
# Date 790946269 -3600
# Node ID e528724951b0c5a2acf368f2c4d0133f555a3b47
# Parent  5c18634db55d97eaa350255c94bb5379354765cf
added optional body priority to binder declaration

diff -r 5c18634db55d -r e528724951b0 doc-src/Ref/defining.tex
--- a/doc-src/Ref/defining.tex	Tue Jan 24 03:04:20 1995 +0100
+++ b/doc-src/Ref/defining.tex	Tue Jan 24 12:17:49 1995 +0100
@@ -620,18 +620,19 @@
 A {\bf binder} is a variable-binding construct such as a quantifier.  The
 constant declaration
 \begin{ttbox}
-\(c\) :: "\(\sigma\)"   (binder "\(\Q\)" \(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
 $x$ is a bound variable of type~$\tau@1$, the body~$P$ has type $\tau@2$
-and the whole term has type~$\tau@3$.  Special characters in $\Q$ must be
-escaped using a single quote.
+and the whole term has type~$\tau@3$. The optional integer $pb$
+specifies the body's priority which defaults to 0.  Special characters
+in $\Q$ must be escaped using a single quote.
 
 The declaration is expanded internally to something like
 \begin{ttbox}
 \(c\)    :: "(\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)"
-"\(\Q\)"\hskip-3pt  :: "[idts, \(\tau@2\)] => \(\tau@3\)"   ("(3\(\Q\)_./ _)" \(p\))
+"\(\Q\)"\hskip-3pt  :: "[idts, \(\tau@2\)] => \(\tau@3\)"   ("(3\(\Q\)_./ _)" [0, \(pb\)] \(p\))
 \end{ttbox}
 Here \ndx{idts} is the nonterminal symbol for a list of identifiers with
 \index{type constraints}