diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/ExPS3.thy
--- a/Nominal/Ex/ExPS3.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/ExPS3.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -9,8 +9,8 @@
 nominal_datatype exp =
   Var "name"
 | App "exp" "exp"
-| Lam x::"name" e::"exp" bind x in e
-| Let x::"name" p::"pat" e1::"exp" e2::"exp" bind (set) x in e2, bind (set) "bp p" in e1
+| Lam x::"name" e::"exp" binds x in e
+| Let x::"name" p::"pat" e1::"exp" e2::"exp" binds (set) x in e2, binds (set) "bp p" in e1
 and pat =
   PVar "name"
 | PUnit