--- a/LMCS-Paper/Paper.thy	Tue Sep 13 19:48:47 2011 +0200
+++ b/LMCS-Paper/Paper.thy	Wed Sep 14 13:40:24 2011 +0900
@@ -1294,8 +1294,8 @@
   \emph{free-atom functions} from the specifications.\footnote{Admittedly, the
   details of our definitions will be somewhat involved. However they are still
   conceptually simple in comparison with the ``positional'' approach taken in
-  Ott \cite[Pages 88--95]{ott-jfp}, which uses the notions of \emph{occurences} and
-  \emph{partial equivalence relations} over sets of occurences.} For the
+  Ott \cite[Pages 88--95]{ott-jfp}, which uses the notions of \emph{occurrences} and
+  \emph{partial equivalence relations} over sets of occurrences.} For the
   \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions
 
   \begin{equation}\label{fvars}

--- a/LMCS-Paper/document/root.tex	Tue Sep 13 19:48:47 2011 +0200
+++ b/LMCS-Paper/document/root.tex	Wed Sep 14 13:40:24 2011 +0900
@@ -72,7 +72,7 @@
 
 \author{Cezary Kaliszyk}
 \address{University of Tsukuba, Japan}
-\email{kaliszyk@score.cs.tsukuba.ac.jp}
+\email{kaliszyk@cs.tsukuba.ac.jp}
 \thanks{$^\star$~This is a revised and expanded version of~\cite{UrbanKaliszyk11}}
 
 \keywords{Nominal Isabelle, variable convention, theorem provers, formal reasoning,lambda-calculus}