diff -r 5ac9a74d22fd -r 2e174807c891 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Mon Sep 27 09:51:15 2010 -0400
+++ b/Nominal/Ex/SingleLet.thy	Mon Sep 27 12:19:17 2010 -0400
@@ -13,7 +13,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 (set) x in t2 
+| Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (res) x in t2 
 and assg =
   As "name" x::"name" t::"trm" bind x in t
 binder
@@ -21,6 +21,8 @@
 where
   "bn (As x y t) = [atom x]"
 
+
+
 thm single_let.distinct
 thm single_let.induct
 thm single_let.inducts
@@ -34,7 +36,7 @@
 thm single_let.supports
 thm single_let.fsupp
 thm single_let.supp
-thm single_let.size
+thm single_let.fresh
 
 
 end