--- a/Nominal/Nominal2_Base.thy	Sun Dec 12 22:09:11 2010 +0000
+++ b/Nominal/Nominal2_Base.thy	Tue Dec 14 14:23:40 2010 +0000
@@ -1835,6 +1835,12 @@
   shows "a \<sharp> b \<longleftrightarrow> a \<noteq> atom b"
   unfolding fresh_def by (simp add: supp_at_base)
 
+lemma fresh_atom_at_base: 
+  fixes b::"'a::at_base"
+  shows "a \<sharp> atom b \<longleftrightarrow> a \<sharp> b"
+  by (simp add: fresh_def supp_at_base supp_atom)
+
+
 instance at_base < fs
 proof qed (simp add: supp_at_base)