diff -r e3f8673085b1 -r 92c001d93225 Nominal/Nominal2_Eqvt.thy
--- a/Nominal/Nominal2_Eqvt.thy	Mon Jan 17 17:20:21 2011 +0100
+++ b/Nominal/Nominal2_Eqvt.thy	Tue Jan 18 06:55:18 2011 +0100
@@ -113,11 +113,6 @@
   shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"
   by (perm_simp add: permute_minus_cancel) (rule refl)
 
-lemma ex1_eqvt[eqvt]:
-  shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
-  unfolding Ex1_def
-  by (perm_simp) (rule refl)
-
 lemma ex1_eqvt2:
   shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))"
   by (perm_simp add: permute_minus_cancel) (rule refl)