--- a/Paper/Paper.thy	Sat May 15 22:06:06 2010 +0100
+++ b/Paper/Paper.thy	Sun May 16 11:00:44 2010 +0100
@@ -1232,7 +1232,7 @@
   \begin{equation}\label{bnemptybinder}
   \mbox{%
   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-  \multicolumn{2}{@ {}l}{\isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\ 
+  \multicolumn{2}{@ {}l}{\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\ 
   $\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} does not occur in @{text "rhs"}
   and the free-variable function for the type of @{text "y"} is @{text "fv_ty"}\\
   $\bullet$ & @{term "v = fv_bn y"} provided @{text "y"} occurs in  @{text "rhs"}