diff -r 53e55a29b788 -r 833d65c6ad88 LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Wed Sep 21 10:24:01 2011 +0200
+++ b/LMCS-Paper/Paper.thy	Wed Sep 21 10:30:10 2011 +0200
@@ -764,7 +764,8 @@
   permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal
   (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.
+  abstract a single atom. In this case they also agree with alpha-equivalence
+  used in older versions of Nominal Isabelle \cite{Urban08}.
 
   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
@@ -1154,12 +1155,12 @@
  
   \begin{equation}\label{letrecs}
   \mbox{%
-  \begin{tabular}{@ {}l@ {}}
+  \begin{tabular}{@ {}l@ {}l}
   \isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\
   \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"} 
-     \;\;\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text t}\\
+     & \hspace{-19mm}\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text t}\\
   \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}
-     \;\;\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\
+     & \hspace{-19mm}\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\
   \isacommand{and} @{text "assn"} $=$\\
   \hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\
   \hspace{5mm}$\mid$~@{text "ACons name trm assn"}\\