--- 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"