--- a/Nominal/Term1.thy	Fri Mar 19 12:24:16 2010 +0100
+++ b/Nominal/Term1.thy	Fri Mar 19 12:28:35 2010 +0100
@@ -195,9 +195,6 @@
 lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}"
 by (simp add: Collect_imp_eq Collect_neg_eq[symmetric])
 
-lemma inf_or: "(infinite x \<or> infinite y) = infinite (x \<union> y)"
-by (simp add: finite_Un)
-
 lemma supp_fv_let:
   assumes sa : "fv_bp bp = supp bp"
   shows "\<lbrakk>fv_trm1 ta = supp ta; fv_trm1 tb = supp tb; fv_bp bp = supp bp\<rbrakk>
@@ -212,7 +209,7 @@
 apply(simp only: permute_ABS)
 apply(simp only: Abs_eq_iff)
 apply(simp only: alpha_gen supp_Pair split_conv eqvts)
-apply(simp only: inf_or[symmetric])
+apply(simp only: infinite_Un)
 apply(simp only: Collect_disj_eq)
 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl)
 apply (simp only: eqvts[symmetric] fv_trm1_eqvt[symmetric])