--- a/Paper/Paper.thy	Tue Apr 27 12:23:06 2010 +0200
+++ b/Paper/Paper.thy	Tue Apr 27 13:44:27 2010 +0200
@@ -1193,20 +1193,20 @@
   %
   \begin{equation}\label{deepbinder}
   \mbox{%
-  \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+  \begin{tabular}{c@ {\hspace{2mm}}p{7.4cm}}
   \multicolumn{2}{@ {}l}{\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\ 
   $\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} is of type @{text "ty"}\smallskip\\
   
-  \multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "x\<^isub>1..x\<^isub>n"}~\isacommand{in}~@{text "y\<^isub>1..y\<^isub>m"}:}\\ 
-  $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m)"}\\ 
-  & \hspace{10mm}@{text "- (fv_aty\<^isub>1 x\<^isub>1 \<union> .. \<union> fv_aty\<^isub>n x\<^isub>n)"}\\ 
+  \multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "x\<^isub>1\<dots>x\<^isub>n"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\ 
+  $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> \<dots> \<union> fv_ty\<^isub>m y\<^isub>m)"}\\ 
+  & \hspace{15mm}@{text "- (fv_aty\<^isub>1 x\<^isub>1 \<union> \<dots> \<union> fv_aty\<^isub>n x\<^isub>n)"}\\ 
   & provided the bodies @{text "y"}$_{1..m}$ are of type @{text "ty"}$_{1..m}$ and the 
   binders @{text "x"}$_{1..n}$ of atomic types @{text "aty"}$_{1..n}$\smallskip\\
   
-  \multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "bn x"}~\isacommand{in}~@{text "y\<^isub>1..y\<^isub>m"}:}\\ 
-  $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m) - (bn x) \<union> (fv_bn x)"}\\
-  $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m) - (bn x)"}\\
-     & provided the @{text "y\<^isub>i"} are of type @{text "ty\<^isub>i"}; the first 
+  \multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "bn x"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\ 
+  $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> \<dots> \<union> fv_ty\<^isub>m y\<^isub>m) - set (bn x) \<union> (fv_bn x)"}\\
+  $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> \<dots> \<union> fv_ty\<^isub>m y\<^isub>m) - set (bn x)"}\\
+     & provided the @{text "y"}$_{1..m}$ are of type @{text "ty"}$_{1..m}$; the first 
     clause applies for @{text x} being a non-recursive deep binder, the 
     second for a recursive deep binder
   \end{tabular}}