--- a/Nominal/Nominal2_Atoms.thy	Thu Mar 18 08:32:55 2010 +0100
+++ b/Nominal/Nominal2_Atoms.thy	Thu Mar 18 09:31:31 2010 +0100
@@ -137,6 +137,12 @@
   and   "(a \<leftrightarrow> b) \<bullet> b = a"
   unfolding permute_flip_at by simp_all
 
+lemma flip_fresh_fresh:
+  fixes a b::"'a::at_base"
+  assumes "atom a \<sharp> x" "atom b \<sharp> x"
+  shows "(a \<leftrightarrow> b) \<bullet> x = x"
+using assms
+by (simp add: flip_def swap_fresh_fresh)
 
 subsection {* Syntax for coercing at-elements to the atom-type *}