Nominal/Ex/SingleLet.thy
changeset 2634 3ce1089cdbf3
parent 2622 e6e6a3da81aa
child 2950 0911cb7bf696
--- 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