--- a/Nominal/Nominal2_Abs.thy	Thu Jan 13 12:12:47 2011 +0000
+++ b/Nominal/Nominal2_Abs.thy	Fri Jan 14 14:22:25 2011 +0000
@@ -545,17 +545,15 @@
 
 lemma Abs_rename_set:
   fixes x::"'a::fs"
-  assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" 
+  assumes a: "(p \<bullet> bs) \<sharp>* x" 
   and     b: "finite bs"
   shows "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
 proof -
-  from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (auto simp add: fresh_star_Pair)   
-  with set_renaming_perm 
-  obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis
+  from b set_renaming_perm 
+  obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast
   have "[bs]set. x =  q \<bullet> ([bs]set. x)"
     apply(rule perm_supp_eq[symmetric])
     using a **
-    unfolding fresh_star_Pair
     unfolding Abs_fresh_star_iff
     unfolding fresh_star_def
     by auto
@@ -566,17 +564,15 @@
 
 lemma Abs_rename_res:
   fixes x::"'a::fs"
-  assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" 
+  assumes a: "(p \<bullet> bs) \<sharp>* x" 
   and     b: "finite bs"
   shows "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
 proof -
-  from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (simp add: fresh_star_Pair) 
-  with set_renaming_perm 
-  obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis
+  from b set_renaming_perm 
+  obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast
   have "[bs]res. x =  q \<bullet> ([bs]res. x)"
     apply(rule perm_supp_eq[symmetric])
     using a **
-    unfolding fresh_star_Pair
     unfolding Abs_fresh_star_iff
     unfolding fresh_star_def
     by auto
@@ -587,17 +583,14 @@
 
 lemma Abs_rename_lst:
   fixes x::"'a::fs"
-  assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" 
+  assumes a: "(p \<bullet> (set bs)) \<sharp>* x" 
   shows "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
 proof -
-  from a have "p \<bullet> (set bs) \<inter> (set bs) = {}" using at_fresh_star_inter 
-    by (simp add: fresh_star_Pair fresh_star_set)
-  with list_renaming_perm 
-  obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by metis 
+  from a list_renaming_perm 
+  obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by blast
   have "[bs]lst. x =  q \<bullet> ([bs]lst. x)"
     apply(rule perm_supp_eq[symmetric])
     using a **
-    unfolding fresh_star_Pair
     unfolding Abs_fresh_star_iff
     unfolding fresh_star_def
     by auto
@@ -611,21 +604,21 @@
 
 lemma Abs_rename_set':
   fixes x::"'a::fs"
-  assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" 
+  assumes a: "(p \<bullet> bs) \<sharp>* x" 
   and     b: "finite bs"
   shows "\<exists>q. [bs]set. x = [q \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
 using Abs_rename_set[OF a b] by metis
 
 lemma Abs_rename_res':
   fixes x::"'a::fs"
-  assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" 
+  assumes a: "(p \<bullet> bs) \<sharp>* x" 
   and     b: "finite bs"
   shows "\<exists>q. [bs]res. x = [q \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
 using Abs_rename_res[OF a b] by metis
 
 lemma Abs_rename_lst':
   fixes x::"'a::fs"
-  assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" 
+  assumes a: "(p \<bullet> (set bs)) \<sharp>* x" 
   shows "\<exists>q. [bs]lst. x = [q \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs"
 using Abs_rename_lst[OF a] by metis