diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/Foo1.thy --- 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' =