--- 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"

--- a/Nominal/nominal_dt_quot.ML	Mon Dec 05 16:12:44 2011 +0000
+++ b/Nominal/nominal_dt_quot.ML	Mon Dec 05 17:05:56 2011 +0000
@@ -487,8 +487,7 @@
    Exists q. [as].x = [p o as].(q o x)  for non-recursive binders 
    Exists q. [as].x = [q o as].(q o x)  for recursive binders
 *)
-fun abs_eq_thm ctxt fprops p parms bn_finite_thms bn_eqvt permute_bns
-  (bclause as (BC (bmode, binders, bodies))) =
+fun abs_eq_thm ctxt fprops p parms bn_eqvt permute_bns (bclause as (BC (bmode, binders, bodies))) =
   case binders of
     [] => [] 
   | _ =>
@@ -510,9 +509,9 @@
           |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t))
           |> HOLogic.mk_Trueprop  
  
-        val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt}
+        val ss = fprops @ @{thms set.simps set_append union_eqvt}
           @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset
-          fresh_star_set} @ @{thms finite.intros finite_fset}
+          fresh_star_set} 
   
         val tac1 = 
           if rec_flag
@@ -548,7 +547,7 @@
                           REPEAT o (etac @{thm conjE})])) [fthm] ctxt 
   
             val abs_eq_thms = flat 
-             (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms bn_eqvt permute_bns) bclauses)
+             (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_eqvt permute_bns) bclauses)
 
             val ((_, eqs), ctxt'') = Obtain.result
               (K (EVERY1