diff -r f6275afb868a -r 6613514ff6cb Nominal/nominal_dt_quot.ML
--- 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