Use the theorem by Brian, requires new Isabelle.
--- a/Quotient-Paper-jv/Paper.thy Tue Jan 31 16:26:36 2012 +0000
+++ b/Quotient-Paper-jv/Paper.thy Fri Feb 03 16:36:18 2012 +0100
@@ -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