--- a/Paper/Paper.thy	Fri May 14 18:12:07 2010 +0100
+++ b/Paper/Paper.thy	Fri May 14 21:18:34 2010 +0100
@@ -937,12 +937,11 @@
   \emph{one} binding clause of a term constructor. 
 
   For binders we distinguish between \emph{shallow} and \emph{deep} binders.
-  Shallow binders are of the form \isacommand{bind}\; {\it labels}\;
-  \isacommand{in}\; {\it labels'} (similar for the other two modes). The
-  restrictions we impose on shallow binders are that in case of
-  \isacommand{bind\_set} and \isacommand{bind\_res} the {\it labels} must
+  Shallow binders are just labels. The
+  restrictions we need to impose on them are that in case of
+  \isacommand{bind\_set} and \isacommand{bind\_res} the labels must
   either refer to atom types or to sets of atom types; in case of
-  \isacommand{bind} we allow labels to refer to atom types or lists of atom types. 
+  \isacommand{bind} the labels must refer to atom types or lists of atom types. 
   Two examples for the use of shallow binders are the specification of
   lambda-terms, where a single name is bound, and type-schemes, where a finite
   set of names is bound:
@@ -1020,10 +1019,10 @@
 
   \begin{center}
   \begin{tabular}{ll}
-  @{text "Foo\<^isub>1 p::pat q::pat t::trm"} & 
-     \isacommand{bind} @{text "bn(p) bn(q)"} \isacommand{in} @{text t}\\
+  @{text "Foo\<^isub>1 p::pat t::trm"} & 
+     \isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\
   @{text "Foo\<^isub>2 x::name p::pat t::trm"} & 
-     \isacommand{bind} @{text "x bn(p)"} \isacommand{in} @{text t}\\ 
+     \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}, ***\\ 
   \end{tabular}
   \end{center}