--- a/Paper/Paper.thy	Thu Mar 18 19:02:33 2010 +0100
+++ b/Paper/Paper.thy	Thu Mar 18 19:39:01 2010 +0100
@@ -133,9 +133,19 @@
   \noindent
   where the $x_i$ are bound in $s$. In this term we might not care about the order in 
   which the $x_i = t_i$ are given, but we do care about the information that there are 
-  as many $x_i$ as there are $t_i$. We lose this information if we represent the $\mathtt{let}$
-  as something 
+  as many $x_i$ as there are $t_i$. We lose this information if we specify the 
+  $\mathtt{let}$-constructor as something like 
+
+  \begin{center}
+  $\LET [x_1,\ldots,x_n].s\; [t_1,\ldots,t_n]$
+  \end{center}
 
+  \noindent
+  where the $[\_].\_$ indicates that a list of variables become bound
+  in $s$. In this representation we need additional predicates to ensure 
+  that the two lists are of equal length. This can result into very 
+  elaborate reasoning (see \cite{BengtsonParow09}). 
+