--- a/Paper/Paper.thy	Thu Dec 09 17:10:08 2010 +0000
+++ b/Paper/Paper.thy	Thu Dec 09 18:12:42 2010 +0000
@@ -517,7 +517,7 @@
   without knowing anything about the structure of @{term x} that
   swapping two fresh atoms, say @{text a} and @{text b}, leaves 
   @{text x} unchanged, namely if @{text "a \<FRESH> x"} and @{text "b \<FRESH> x"}
-  then @{term "(a \<rightleftharpoons> b) \<bullet> x"}.
+  then @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
   %
   %\begin{myproperty}\label{swapfreshfresh}
   %@{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
@@ -1136,7 +1136,7 @@
   that the term-constructors @{text PVar} and @{text PTup} may
   not have a binding clause (all arguments are used to define @{text "bn"}).
   In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons}
-  may have a binding clause involving the argument @{text t} (the only one that
+  may have a binding clause involving the argument @{text trm} (the only one that
   is \emph{not} used in the definition of the binding function). This restriction
   is sufficient for lifting the binding function to $\alpha$-equated terms.
 
@@ -1186,8 +1186,7 @@
   Therefore we will first
   extract ``raw'' datatype definitions from the specification and then define 
   explicitly an $\alpha$-equivalence relation over them. We subsequently
-  quotient the datatypes according to our $\alpha$-equivalence.
-
+  construct the quotient of the datatypes according to our $\alpha$-equivalence.
 
   The ``raw'' datatype definition can be obtained by stripping off the 
   binding clauses and the labels from the types. We also have to invent