diff -r f6275afb868a -r 6613514ff6cb Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Mon Dec 05 16:12:44 2011 +0000
+++ b/Nominal/Nominal2_Abs.thy	Mon Dec 05 17:05:56 2011 +0000
@@ -879,17 +879,16 @@
 
 subsection {* Renaming of bodies of abstractions *}
 
-(* FIXME: finiteness assumption is not needed *)
-
 lemma Abs_rename_set:
   fixes x::"'a::fs"
   assumes a: "(p \<bullet> bs) \<sharp>* x" 
-  and     b: "finite bs"
+  (*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 set_renaming_perm2 
   obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast
-  have ***: "q \<bullet> bs = p \<bullet> bs" using b * by (induct) (simp add: permute_set_eq, simp add: insert_eqvt)
+  have ***: "q \<bullet> bs = p \<bullet> bs" using *
+    unfolding permute_set_eq_image image_def by auto
   have "[bs]set. x =  q \<bullet> ([bs]set. x)"
     apply(rule perm_supp_eq[symmetric])
     using a **
@@ -904,12 +903,13 @@
 lemma Abs_rename_res:
   fixes x::"'a::fs"
   assumes a: "(p \<bullet> bs) \<sharp>* x" 
-  and     b: "finite bs"
+  (*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 set_renaming_perm2 
   obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast
-  have ***: "q \<bullet> bs = p \<bullet> bs" using b * by (induct) (simp add: permute_set_eq, simp add: insert_eqvt)
+  have ***: "q \<bullet> bs = p \<bullet> bs" using * 
+    unfolding permute_set_eq_image image_def by auto
   have "[bs]res. x =  q \<bullet> ([bs]res. x)"
     apply(rule perm_supp_eq[symmetric])
     using a **
@@ -946,16 +946,16 @@
 lemma Abs_rename_set':
   fixes x::"'a::fs"
   assumes a: "(p \<bullet> bs) \<sharp>* x" 
-  and     b: "finite bs"
+  (*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
+using Abs_rename_set[OF a] by metis
 
 lemma Abs_rename_res':
   fixes x::"'a::fs"
   assumes a: "(p \<bullet> bs) \<sharp>* x" 
-  and     b: "finite bs"
+  (*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
+using Abs_rename_res[OF a] by metis
 
 lemma Abs_rename_lst':
   fixes x::"'a::fs"