--- a/Nominal/Nominal2_Base.thy	Fri Apr 19 00:10:52 2013 +0100
+++ b/Nominal/Nominal2_Base.thy	Tue Jun 04 09:39:23 2013 +0100
@@ -354,7 +354,6 @@
   unfolding permute_atom_def
   by (metis Rep_perm_ext ext)
 
-
 subsection {* Permutations for permutations *}
 
 instantiation perm :: pt
@@ -1001,6 +1000,11 @@
   shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
   unfolding Un_def by simp
 
+lemma UNION_eqvt [eqvt]:
+  shows "p \<bullet> (UNION A f) = (UNION (p \<bullet> A) (p \<bullet> f))"
+unfolding UNION_eq
+by (perm_simp) (simp)
+
 lemma Diff_eqvt [eqvt]:
   fixes A B :: "'a::pt set"
   shows "p \<bullet> (A - B) = (p \<bullet> A) - (p \<bullet> B)"
@@ -1603,6 +1607,17 @@
     by blast
 qed
 
+lemma perm_eq_iff2:
+  fixes p q :: "perm"
+  shows "p = q \<longleftrightarrow> (\<forall>a::atom \<in> supp p \<union> supp q. p \<bullet> a = q \<bullet> a)"
+  unfolding perm_eq_iff
+  apply(auto)
+  apply(case_tac "a \<sharp> p \<and> a \<sharp> q")
+  apply(simp add: fresh_perm)
+  apply(simp add: fresh_def)
+  done
+
+
 instance perm :: fs
 by default (simp add: supp_perm finite_perm_lemma)
 
@@ -2017,15 +2032,13 @@
   assumes fin: "finite S"
   shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S"
 proof -
-  have eqvt: "eqvt (\<lambda>S. \<Union> supp ` S)" 
-    unfolding eqvt_def 
-    by (perm_simp) (simp)
+  have eqvt: "eqvt (\<lambda>S. \<Union>x \<in> S. supp x)" 
+    unfolding eqvt_def by simp 
   have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"
     by (rule supp_finite_atom_set[symmetric]) (rule Union_of_finite_supp_sets[OF fin])
-  also have "\<dots> = supp ((\<lambda>S. \<Union> supp ` S) S)" by simp
   also have "\<dots> \<subseteq> supp S" using eqvt
     by (rule supp_fun_app_eqvt)
-  finally show "(\<Union>x\<in>S. supp x) \<subseteq> supp S" .
+  finally show "(\<Union>x\<in>S. supp x) \<subseteq> supp S" .  
 qed
 
 lemma supp_of_finite_sets: