--- a/Nominal/Nominal2_Abs.thy	Wed Feb 16 14:44:33 2011 +0000
+++ b/Nominal/Nominal2_Abs.thy	Thu Feb 24 16:26:11 2011 +0000
@@ -768,6 +768,15 @@
   unfolding fresh_star_def
   by(auto simp add: Abs_fresh_iff)
 
+lemma Abs_fresh_star2:
+  fixes x::"'a::fs"
+  shows "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* Abs_set bs x \<longleftrightarrow> as \<sharp>* x"
+  and   "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* Abs_res bs x \<longleftrightarrow> as \<sharp>* x"
+  and   "cs \<inter> set ds = {} \<Longrightarrow> cs \<sharp>* Abs_lst ds x \<longleftrightarrow> cs \<sharp>* x"
+  unfolding fresh_star_def Abs_fresh_iff
+  by auto
+
+
 lemma Abs1_eq:
   fixes x::"'a::fs"
   shows "Abs_set {a} x = Abs_set {a} y \<longleftrightarrow> x = y"