--- a/LMCS-Paper/Paper.thy	Wed Sep 21 12:23:32 2011 +0200
+++ b/LMCS-Paper/Paper.thy	Wed Sep 21 15:18:32 2011 +0200
@@ -765,7 +765,9 @@
   (similarly for $\approx_{\,\textit{list}}$).  It can also relatively easily be
   shown that all three notions of alpha-equivalence coincide, if we only
   abstract a single atom. In this case they also agree with the alpha-equivalence
-  used in older versions of Nominal Isabelle \cite{Urban08}.
+  used in older versions of Nominal Isabelle \cite{Urban08}.\footnote{We omit a
+  proof of this fact since the details are hairy and not really important for the
+  purpose of this paper.}
 
   In the rest of this section we are going to show that the alpha-equivalences
   really lead to abstractions where some atoms are bound (or more precisely