--- a/Quot/Nominal/Nominal2_Supp.thy	Mon Feb 01 16:13:24 2010 +0100
+++ b/Quot/Nominal/Nominal2_Supp.thy	Mon Feb 01 16:23:47 2010 +0100
@@ -66,12 +66,6 @@
   which 'translates' between both sets.
 *}
 
-lemma swap_set_fresh:
-  assumes a: "a \<notin> S" "b \<notin> S"
-  shows "(a \<rightleftharpoons> b) \<bullet> S = S"
-  using a
-  by (auto simp add: permute_set_eq swap_atom)
-
 lemma at_set_avoiding_aux:
   fixes Xs::"atom set"
   and   As::"atom set"
@@ -107,7 +101,7 @@
       unfolding insert_eqvt
       using `p \<bullet> x = x` `sort_of y = sort_of x`
       using `x \<notin> p \<bullet> Xs` `y \<notin> p \<bullet> Xs`
-      by (simp add: swap_atom swap_set_fresh)
+      by (simp add: swap_atom swap_set_not_in)
     have "?q \<bullet> insert x Xs \<inter> As = {}"
       using `y \<notin> As` `p \<bullet> Xs \<inter> As = {}`
       unfolding q by simp
@@ -353,9 +347,9 @@
   shows "supp S = S"
   apply(rule finite_supp_unique)
   apply(simp add: supports_def)
-  apply(auto simp add: permute_set_eq_vimage vimage_def swap_atom)[1]
+  apply(simp add: swap_set_not_in)
   apply(rule assms)
-  apply(auto simp add: permute_set_eq swap_atom)[1]
+  apply(simp add: swap_set_in)
 done