diff -r 811add8917aa -r 419041034e35 thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Fri May 20 10:27:11 2016 +0100
+++ b/thys/Paper/Paper.thy	Fri May 20 10:30:24 2016 +0100
@@ -1246,7 +1246,7 @@
   \noindent
   {\bf Acknowledgements:}
   We are very grateful to Martin Sulzmann for his comments on our work and 
-  moreover patiently explaining to us the details in \cite{Sulzmann2014}. We
+  moreover for patiently explaining to us the details in \cite{Sulzmann2014}. We
   also received very helpful comments from James Cheney and anonymous referees.
   \small
   \bibliographystyle{plain}