# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1274004044 -3600
# Node ID b9292bbcffb6f169b98c4f0ba21f160e00237cfa
# Parent  8beda0b4e35a4a5cd38af285f8f0e3453b5a73ef
tuned paper

diff -r 8beda0b4e35a -r b9292bbcffb6 Paper/Paper.thy
--- 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"}