--- a/Nominal/Ex/SingleLet.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/SingleLet.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -7,13 +7,13 @@
 nominal_datatype single_let: trm =
   Var "name"
 | App "trm" "trm"
-| Lam x::"name" t::"trm"  bind x in t
-| Let a::"assg" t::"trm"  bind "bn a" in t
-| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2
-| Bar x::"name" y::"name" t::"trm" bind y x in t x y
-| Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (set+) x in t2 
+| Lam x::"name" t::"trm"  binds x in t
+| Let a::"assg" t::"trm"  binds "bn a" in t
+| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" binds (set) x in y t t1 t2
+| Bar x::"name" y::"name" t::"trm" binds y x in t x y
+| Baz x::"name" t1::"trm" t2::"trm" binds (set) x in t1, binds (set+) x in t2 
 and assg =
-  As "name" x::"name" t::"trm" bind x in t
+  As "name" x::"name" t::"trm" binds x in t
 binder
   bn::"assg \<Rightarrow> atom list"
 where