--- a/LMCS-Paper/Paper.thy	Wed Sep 21 12:01:34 2011 +0200
+++ b/LMCS-Paper/Paper.thy	Wed Sep 21 12:08:03 2011 +0200
@@ -2154,7 +2154,7 @@
   for @{text "c"} (third line); for @{text "Let_pat\<^sup>\<alpha>"} we can assume
   all bound atoms from an assignment are fresh for @{text "c"} (fourth
   line). In order to see how an instantiation for @{text "c"} in the
-  conclusion `controls' the premises, you have to take into account that
+  conclusion `controls' the premises, one has to take into account that
   Isabelle/HOL is a typed logic. That means if @{text "c"} is instantiated
   with a pair, for example, then this type-constraint will be propagated to
   the premises. The main point is that if @{text "c"} is instantiated