diff -r 8d65817a52f7 -r 373cd788d327 Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Mar 23 17:22:37 2010 +0100
+++ b/Paper/Paper.thy	Tue Mar 23 17:44:43 2010 +0100
@@ -537,8 +537,8 @@
   $bn_{\alpha{}1}$, \ldots $bn_{\alpha{}m}$. They are schematically written as
   follows:
 
-  \begin{center}
-  \begin{tabular}{@ {\hspace{-9mm}}p{1.8cm}l}
+  \begin{equation}\label{scheme}
+  \mbox{\begin{tabular}{@ {\hspace{-9mm}}p{1.8cm}l}
   type \mbox{declaration part} &
   $\begin{cases}
   \mbox{\begin{tabular}{l}
@@ -557,8 +557,8 @@
   $\ldots$\\
   \end{tabular}}
   \end{cases}$\\
-  \end{tabular}
-  \end{center}
+  \end{tabular}}
+  \end{equation}
 
   \noindent
   Every type declaration $ty_{\alpha{}i}$ consists of a collection of 
@@ -606,31 +606,50 @@
   \hspace{5mm}\phantom{$\mid$} TVar\;{\it name}\\
   \hspace{5mm}$\mid$ TFun\;{\it ty}\;{\it ty}\\
   \isacommand{and} {\it tsc} = All\;{\it xs::(name fset)}\;{\it T::ty}\\
-  \hspace{22mm}\isacommand{bind\_res} {\it xs} \isacommand{in} {\it T}\\
+  \hspace{24mm}\isacommand{bind\_res} {\it xs} \isacommand{in} {\it T}\\
   \end{tabular}
   \end{tabular}
   \end{center}
 
   \noindent
-  A \emph{deep} binder uses an auxiliary binding function that picks out the atoms
-  that are bound in one or more arguments. This binding function returns either 
+  A \emph{deep} binder uses an auxiliary binding function that ``picks'' out the atoms
+  in one argument that can be bound in one or more arguments. Such a binding function returns either 
   a set of atoms (for \isacommand{bind\_set} and \isacommand{bind\_res}) or a 
-  list of atoms (for \isacommand{bind}). Such binding functions can be defined 
-  by primitive recursion over the corresponding type. They are defined by equations
-  included in the binding function part of the scheme given above. 
+  list of atoms (for \isacommand{bind}). It can be defined 
+  by primitive recursion over the corresponding type; the equations
+  are stated in the binding function part of the scheme shown in \eqref{scheme}. 
+
+  In the present version of Nominal Isabelle, we 
+  adopted the restrictions the Ott-tool imposes on the binding functions, namely a 
+  binding functions can only return the empty set, a singleton set of atoms or 
+  unions of atom sets. For example for lets with patterns you might define
 
-  For the moment we
-  adopt the restriction of the Ott-tool that binding functions can only return
-  the empty set, a singleton set of atoms or unions of atom sets. For example
-  
-  over the type for which they specify the bound atoms. 
+  \begin{center}
+  \begin{tabular}{l}
+  \isacommand{nominal\_datatype} {\it trm} =\\
+  \hspace{5mm}\phantom{$\mid$} Var\;{\it name}\\
+  \hspace{5mm}$\mid$ App\;{\it trm}\;{\it trm}\\
+  \hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::trm} 
+     \;\;\isacommand{bind} {\it x} \isacommand{in} {\it t}\\
+  \hspace{5mm}$\mid$ Let\;{\it p::pat}\;{\it trm}\; {\it t::trm} 
+     \;\;\isacommand{bind} {\it bn(p)} \isacommand{in} {\it t}\\
+  \isacommand{and} {\it pat} =\\
+  \hspace{5mm}\phantom{$\mid$} PNo\\
+  \hspace{5mm}$\mid$ PVr\;{\it name}\\
+  \hspace{5mm}$\mid$ PPr\;{\it pat}\;{\it pat}\\ 
+  \isacommand{with} {\it bn::pat $\Rightarrow$ atom set}\\
+  \isacommand{where} $bn(\textrm{PNo}) = \varnothing$\\
+  \hspace{5mm}$\mid$ $bn(\textrm{PVr}\;x) = \{atom\; x\}$\\
+  \hspace{5mm}$\mid$ $bn(\textrm{PPr}\;p_1\;p_2) = bn(p_1) \cup bn(p_2)$\\ 
+  \end{tabular}
+  \end{center}
   
-
+  \noindent
+  In this definition the function $atom$ coerces a name into the generic 
+  atom type of Nominal Isabelle. In this way we can treat binders of different
+  type uniformely.
 
-  \noindent
-  A specification of a term-calculus in Nominal Isabelle is very similar to 
-  the usual datatype definition of Isabelle/HOL: 
-
+  
 
   Because of the problem Pottier pointed out in \cite{Pottier06}, the general 
   binders from the previous section cannot be used directly to represent w