--- a/Nominal/Nominal2_Abs.thy	Fri Nov 26 10:53:55 2010 +0000
+++ b/Nominal/Nominal2_Abs.thy	Fri Nov 26 19:03:23 2010 +0000
@@ -525,11 +525,11 @@
 
 lemma Abs_fresh_star:
   fixes x::"'a::fs"
-  shows "as \<sharp>* Abs_set as x"
-  and   "as \<sharp>* Abs_res as x"
-  and   "set bs \<sharp>* Abs_lst bs x"
+  shows "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_set as' x"
+  and   "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_res as' x"
+  and   "bs \<subseteq> set bs' \<Longrightarrow> bs \<sharp>* Abs_lst bs' x"
   unfolding fresh_star_def
-  by(simp_all add: Abs_fresh_iff)
+  by(auto simp add: Abs_fresh_iff)
 
 
 section {* Infrastructure for building tuples of relations and functions *}