--- a/Nominal/Nominal2_Eqvt.thy	Tue Jan 18 22:11:49 2011 +0900
+++ b/Nominal/Nominal2_Eqvt.thy	Tue Jan 18 17:19:50 2011 +0100
@@ -36,7 +36,7 @@
   Pair_eqvt permute_list.simps permute_option.simps
 
   (* sets *)
-  mem_eqvt empty_eqvt insert_eqvt set_eqvt
+  mem_eqvt empty_eqvt insert_eqvt set_eqvt inter_eqvt
 
   (* fsets *)
   permute_fset fset_eqvt
@@ -173,11 +173,6 @@
   unfolding Un_def
   by (perm_simp) (rule refl)
 
-lemma inter_eqvt[eqvt]:
-  shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
-  unfolding Int_def 
-  by (perm_simp) (rule refl)
-
 lemma Diff_eqvt[eqvt]:
   fixes A B :: "'a::pt set"
   shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B"