diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/Foo2.thy
--- a/Nominal/Ex/Foo2.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/Foo2.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -13,9 +13,9 @@
 nominal_datatype foo: trm =
   Var "name"
 | App "trm" "trm"
-| Lam x::"name" t::"trm"  bind x in t
-| Let1 a1::"assg" t1::"trm" a2::"assg" t2::"trm" bind "bn a1" in t1, bind "bn a2" in t2
-| Let2 x::"name" y::"name" t1::"trm" t2::"trm" bind x y in t1, bind y in t2
+| Lam x::"name" t::"trm"  binds x in t
+| Let1 a1::"assg" t1::"trm" a2::"assg" t2::"trm" binds "bn a1" in t1, binds "bn a2" in t2
+| Let2 x::"name" y::"name" t1::"trm" t2::"trm" binds x y in t1, binds y in t2
 and assg =
   As_Nil
 | As "name" x::"name" t::"trm" "assg"