--- a/ESOP-Paper/Paper.thy	Thu Jun 30 02:19:59 2011 +0100
+++ b/ESOP-Paper/Paper.thy	Thu Jun 30 11:05:25 2011 +0100
@@ -1997,7 +1997,7 @@
 
   The @{text Let}-case involving a (non-recursive) deep binder is a bit more complicated.
   The reason is that the we cannot apply Property \ref{avoiding} to the whole term @{text "Let p t"},
-  because @{text p} might contain names that are bound (by @{text bn}) and so are 
+  because @{text p} might contain names bound by @{text bn}, but also some that are 
   free. To solve this problem we have to introduce a permutation function that only
   permutes names bound by @{text bn} and leaves the other names unchanged. We do this again
   by lifting. For a