--- a/Nominal/Abs.thy	Fri Mar 19 12:24:16 2010 +0100
+++ b/Nominal/Abs.thy	Fri Mar 19 12:28:35 2010 +0100
@@ -782,5 +782,10 @@
   \<and> pi \<bullet> bs = cs)"
 by (simp add: alpha_gen)
 
+(* maybe should be added to Infinite.thy *)
+lemma infinite_Un:
+  shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
+  by simp
+
 end
 

--- a/Nominal/LamEx.thy	Fri Mar 19 12:24:16 2010 +0100
+++ b/Nominal/LamEx.thy	Fri Mar 19 12:28:35 2010 +0100
@@ -41,10 +41,6 @@
   "\<not>(P \<and> Q) \<longleftrightarrow> (\<not>P) \<or> (\<not>Q)"
   by simp
 
-lemma infinite_Un:
-  "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
-  by simp
-
 instance
 apply default
 apply(induct_tac x)

--- a/Nominal/LamEx2.thy	Fri Mar 19 12:24:16 2010 +0100
+++ b/Nominal/LamEx2.thy	Fri Mar 19 12:28:35 2010 +0100
@@ -41,10 +41,6 @@
   "\<not>(P \<and> Q) \<longleftrightarrow> (\<not>P) \<or> (\<not>Q)"
   by simp
 
-lemma infinite_Un:
-  "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
-  by simp
-
 instance
 apply default
 apply(induct_tac x)

--- 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])