--- a/Quotient-Paper-jv/Paper.thy	Fri Feb 03 15:47:47 2012 +0000
+++ b/Quotient-Paper-jv/Paper.thy	Fri Feb 03 15:51:55 2012 +0000
@@ -325,7 +325,7 @@
   of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation}
   from Homeier \cite{Homeier05}.
 
-  {\bf EXAMPLE BY HUFFMAN ABOUT @{thm map_concat}}
+  {\bf EXAMPLE BY HUFFMAN @{thm map_concat_fset[no_vars]}}
 
   In addition we are able to clearly specify what is involved
   in the lifting process (this was only hinted at in \cite{Homeier05} and
@@ -437,7 +437,7 @@
 
   \begin{definition}[Bounded $\forall$ and $\lambda$]\label{def:babs}
   @{text "\<forall>x \<in> S. P x"} holds if for all @{text x}, @{text "x \<in> S"} implies @{text "P x"};
-  and @{text "(\<lambda>x \<in> S. f x) = f x"} provided @{text "x \<in> S"}.
+  and @{text "(\<lambda>x \<in> S. f x) x = f x"} provided @{text "x \<in> S"}.
   \end{definition}
 
   The central definition in Homeier's work \cite{Homeier05} relates equivalence
@@ -1294,7 +1294,7 @@
 
   \begin{isabelle}\ \ \ \ \ %
   \begin{tabular}{@ {}l}
-  \isacommand{fun}~~@{text "int_rel :: (nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"}\\
+  \isacommand{fun}~~@{text "int_rel :: (nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"}\\
   \isacommand{where}~~@{text "int_rel (m, n) (p, q) = (m + q = n + p)"}
   \end{tabular}
   \end{isabelle}

--- a/Quotient-Paper/Paper.thy	Fri Feb 03 15:47:47 2012 +0000
+++ b/Quotient-Paper/Paper.thy	Fri Feb 03 15:51:55 2012 +0000
@@ -428,7 +428,7 @@
 
   \begin{definition}[Bounded $\forall$ and $\lambda$]\label{def:babs}
   @{text "\<forall>x \<in> S. P x"} holds if for all @{text x}, @{text "x \<in> S"} implies @{text "P x"};
-  and @{text "(\<lambda>x \<in> S. f x) = f x"} provided @{text "x \<in> S"}.
+  and @{text "(\<lambda>x \<in> S. f x) x = f x"} provided @{text "x \<in> S"}.
   \end{definition}
 
   The central definition in Homeier's work \cite{Homeier05} relates equivalence 
@@ -1284,7 +1284,7 @@
 
   \begin{isabelle}\ \ \ \ \ %
   \begin{tabular}{@ {}l}
-  \isacommand{fun}~~@{text "int_rel :: (nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"}\\
+  \isacommand{fun}~~@{text "int_rel :: (nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"}\\
   \isacommand{where}~~@{text "int_rel (m, n) (p, q) = (m + q = n + p)"}
   \end{tabular}
   \end{isabelle}