diff -r d1d09177ec89 -r 3ce1089cdbf3 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Fri Dec 31 13:31:39 2010 +0000 +++ b/Nominal/Ex/SingleLet.thy Fri Dec 31 15:37:04 2010 +0000 @@ -11,7 +11,7 @@ | 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 (res) x in t2 +| Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (set+) x in t2 and assg = As "name" x::"name" t::"trm" bind x in t binder