--- a/ESOP-Paper/Paper.thy	Mon Jun 20 20:09:51 2011 +0900
+++ b/ESOP-Paper/Paper.thy	Tue Jun 21 10:39:25 2011 +0900
@@ -1715,7 +1715,7 @@
   any bound atoms. In Ott, in contrast, the user may 
   define @{text "bn"}$_{1..m}$ so that they return bound
   atoms and in this case the third implication is \emph{not} true. A 
-  result is that the lifing of the corresponding binding functions in Ott to $\alpha$-equated
+  result is that the lifting of the corresponding binding functions in Ott to $\alpha$-equated
   terms is impossible.
 
   Having established respectfulness for the raw term-constructors, the