diff -r 4648bd6930e4 -r ac3d4e4f5cbe Nominal/Ex/SingleLetFoo.thy
--- a/Nominal/Ex/SingleLetFoo.thy	Fri May 14 15:02:25 2010 +0100
+++ b/Nominal/Ex/SingleLetFoo.thy	Fri May 14 15:21:05 2010 +0100
@@ -14,6 +14,7 @@
 | Let a::"assg" t::"trm"  bind_set "bn a" in t
 | Foo1 a1::"assg" a2::"assg" t::"trm" bind_set "bn a1" "bn a2" in t
 | Foo2 x::name a::"assg" t::"trm" bind_set x "bn a" in t
+
 and assg =
   As "name" "trm"
 binder
@@ -25,6 +26,7 @@
 thm trm_assg.eq_iff
 thm trm_assg.supp
 thm trm_assg.perm
+thm trm_assg.fv[simplified trm_assg.supp(1-2),no_vars]
 
 thm permute_trm_raw_permute_assg_raw.simps
 thm fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps[no_vars]