--- a/Nominal/Nominal2_Base.thy	Wed Feb 16 14:44:33 2011 +0000
+++ b/Nominal/Nominal2_Base.thy	Thu Feb 24 16:26:11 2011 +0000
@@ -1654,7 +1654,6 @@
 done
 
 lemma fresh_star_atom_set_conv:
-  fixes p::"perm"
   assumes fresh: "as \<sharp>* bs"
   and     fin: "finite as" "finite bs"
   shows "bs \<sharp>* as"
@@ -1662,6 +1661,13 @@
 unfolding fresh_star_def fresh_def
 by (auto simp add: supp_finite_atom_set fin)
 
+lemma atom_fresh_star_disjoint:
+  assumes fin: "finite bs" 
+  shows "as \<sharp>* bs \<longleftrightarrow> (as \<inter> bs = {})"
+
+unfolding fresh_star_def fresh_def
+by (auto simp add: supp_finite_atom_set fin)
+
 
 lemma fresh_star_Pair:
   shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" 
@@ -1747,14 +1753,6 @@
 apply(simp add: imp_eqvt fresh_eqvt mem_eqvt)
 done
 
-lemma at_fresh_star_inter:
-  assumes a: "(p \<bullet> bs) \<sharp>* bs" 
-  and     b: "finite bs"
-  shows "p \<bullet> bs \<inter> bs = {}"
-using a b
-unfolding fresh_star_def
-unfolding fresh_def
-by (auto simp add: supp_finite_atom_set)
 
 
 section {* Induction principle for permutations *}