Not much progress about the single existential let case.
\documentstyle[epsf]{acmconf}\usepackage{isabelle,isabellesym}% further packages required for unusual symbols (see also% isabellesym.sty), use only when needed%\usepackage{amssymb} %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>, %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>, %\<triangleq>, \<yen>, \<lozenge>%\usepackage[greek,english]{babel} %option greek for \<euro> %option english (default language) for \<guillemotleft>, \<guillemotright>%\usepackage[latin1]{inputenc} %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>, %\<threesuperior>, \<threequarters>, \<degree>%\usepackage[only,bigsqcap]{stmaryrd} %for \<Sqinter>%\usepackage{eufrak} %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)%\usepackage{textcomp} %for \<cent>, \<currency>% this should be the last package used\usepackage{pdfsetup}% urls in roman style, theory text in math-similar italics\urlstyle{rm}\isabellestyle{it}% for uniform font size%\renewcommand{\isastyle}{\isastyleminor}%----------------- theorem definitions ----------\newtheorem{Theorem}{Theorem}[section]\newtheorem{Definition}[Theorem]{Definition}\newtheorem{Example}{\it Example}[section]%-------------------- environment definitions -----------------\newenvironment{example}[0]{\begin{Example} \it}{\end{Example}}\newenvironment{proof-of}[1]{{\em Proof of #1:}}{}\begin{document}\title{\LARGE\bf General Binding Structures in Nominal Isabelle, or How to Formalise Core-Haskell}\maketitle\maketitle\begin{abstract} TODO\end{abstract}% generated text of all theories\input{session}%\bibliographystyle{plain}% optional bibliography%\bibliographystyle{abbrv}%\bibliography{root}\end{document}%%% Local Variables:%%% mode: latex%%% TeX-master: t%%% End: