--- a/Nominal/Nominal2_Base.thy	Fri Mar 11 08:51:39 2011 +0000
+++ b/Nominal/Nominal2_Base.thy	Mon Mar 14 16:35:59 2011 +0100
@@ -810,17 +810,17 @@
 
 declare imp_eqvt[folded induct_implies_def, eqvt]
 
+lemma all_eqvt [eqvt]:
+  shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
+  unfolding All_def
+  by (perm_simp) (rule refl)
+
+declare all_eqvt[folded induct_forall_def, eqvt]
+
 lemma ex_eqvt [eqvt]:
   shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)"
-  unfolding permute_fun_def permute_bool_def
-  by (auto, rule_tac x="p \<bullet> x" in exI, simp)
-
-lemma all_eqvt [eqvt]:
-  shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
-  unfolding permute_fun_def permute_bool_def
-  by (auto, drule_tac x="p \<bullet> x" in spec, simp)
-
-declare all_eqvt[folded induct_forall_def, eqvt]
+  unfolding Ex_def
+  by (perm_simp) (rule refl)
 
 lemma ex1_eqvt [eqvt]:
   shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
@@ -2559,6 +2559,13 @@
 apply(auto)
 done
 
+(* FIXME 
+lemma supp_cofinite_set_at_base:
+  assumes a: "finite (UNIV - S)"
+  shows "supp S = atom ` (UNIV - S)"
+apply(rule finite_supp_unique)
+*)
+
 lemma fresh_finite_set_at_base:
   fixes a::"'a::at_base"
   assumes a: "finite S"