--- a/LMCS-Paper/Paper.thy	Mon Sep 19 21:52:59 2011 +0200
+++ b/LMCS-Paper/Paper.thy	Tue Sep 20 14:44:50 2011 +0900
@@ -2414,7 +2414,7 @@
   Another technique for representing binding is higher-order abstract syntax
   (HOAS), which for example is implemented in the Twelf system \cite{pfenningsystem}. 
   This representation technique supports very elegantly many aspects of
-  \emph{single} binding, and impressive work by Lee et al ~\cite{LeeCraryHarper07} 
+  \emph{single} binding, and impressive work by Lee et al~\cite{LeeCraryHarper07} 
   has been done that uses HOAS for mechanising the metatheory of SML. We
   are, however, not aware how multiple binders of SML are represented in this
   work. Judging from the submitted Twelf-solution for the POPLmark challenge,