--- a/Nominal/Abs.thy	Thu Mar 11 19:43:50 2010 +0100
+++ b/Nominal/Abs.thy	Thu Mar 11 20:49:31 2010 +0100
@@ -736,7 +736,7 @@
 apply(simp add: inj_on_def)
 done
 
-lemma
+lemma supp_atom_image:
   fixes as::"'a::at_base set"
   shows "supp (atom ` as) = supp as"
 apply(simp add: supp_def)
@@ -745,6 +745,12 @@
 apply(simp add: atom_image_cong)
 done
 
+lemma swap_atom_image_fresh: "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn"
+  apply (simp add: fresh_def)
+  apply (simp add: supp_atom_image)
+  apply (fold fresh_def)
+  apply (simp add: swap_fresh_fresh)
+  done
 
 
 end