--- a/Nominal/Ex/Foo1.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/Foo1.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -13,11 +13,11 @@
 nominal_datatype foo: trm =
   Var "name"
 | App "trm" "trm"
-| Lam x::"name" t::"trm"  bind x in t
-| Let1 a::"assg" t::"trm"  bind "bn1 a" in t
-| Let2 a::"assg" t::"trm"  bind "bn2 a" in t
-| Let3 a::"assg" t::"trm"  bind "bn3 a" in t
-| Let4 a::"assg'" t::"trm"  bind (set) "bn4 a" in t
+| Lam x::"name" t::"trm"    binds x in t
+| Let1 a::"assg" t::"trm"   binds "bn1 a" in t
+| Let2 a::"assg" t::"trm"   binds "bn2 a" in t
+| Let3 a::"assg" t::"trm"   binds "bn3 a" in t
+| Let4 a::"assg'" t::"trm"  binds (set) "bn4 a" in t
 and assg =
   As "name" "name" "trm"
 and assg' =