--- a/Paper/Paper.thy	Tue Mar 23 11:52:55 2010 +0100
+++ b/Paper/Paper.thy	Tue Mar 23 13:03:42 2010 +0100
@@ -580,20 +580,25 @@
   lambda-terms and type-schemes use them:
 
   \begin{center}
-  \begin{tabular}{cc}
-  \begin{tabular}{l}
-  \isacommand{nominal\_datatype} lam =\\
-  \hspace{5mm}Var\;{\it name}\\
-  \hspace{5mm}App\;{\it lam}\;{\it lam}\\
-  \hspace{5mm}Lam\;{\it x::name}\;{\it t::lam}\;
-  \isacommand{bind} {\it x} \isacommand{in} {\it t}\\
+  \begin{tabular}{@ {}cc@ {}}
+  \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
+  \isacommand{nominal\_datatype} {\it lam} =\\
+  \hspace{5mm}\phantom{$\mid$} Var\;{\it name}\\
+  \hspace{5mm}$\mid$ App\;{\it lam}\;{\it lam}\\
+  \hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::lam}\\
+  \hspace{22mm}\isacommand{bind} {\it x} \isacommand{in} {\it t}\\
   \end{tabular} &
-  \begin{tabular}{l}
-  foo
+  \begin{tabular}{@ {}l@ {}}
+  \isacommand{nominal\_datatype} {\it ty} =\\
+  \hspace{5mm}\phantom{$\mid$} TVar\;{\it name}\\
+  \hspace{5mm}$\mid$ TFun\;{\it ty}\;{\it ty}\\
+  \isacommand{and} {\it S} = All\;{\it xs::(name fset)}\;{\it T::ty}\\
+  \hspace{27mm}\isacommand{bind} {\it xs} \isacommand{in} {\it T}\\
   \end{tabular}
   \end{tabular}
   \end{center}
 
+  \noindent
   A specification of a term-calculus in Nominal Isabell is very similar to 
   the usual datatype definition of Isabelle/HOL: