--- a/Quot/Nominal/Nominal2_Supp.thy	Mon Feb 01 16:05:59 2010 +0100
+++ b/Quot/Nominal/Nominal2_Supp.thy	Mon Feb 01 20:02:44 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
@@ -345,23 +339,21 @@
   using not_fresh_nat_of [unfolded fresh_def] by auto
 
 
-(*
-section {* Characterisation of the support of sets of atoms *}
+section {* Support for sets of atoms *}
 
-lemma swap_set_ineq:
-  fixes a b::"'a::at"
-  assumes "a \<in> S" "b \<notin> S"
-  shows "(a \<leftrightarrow> b) \<bullet> S \<noteq> S"
-using assms
-unfolding permute_set_eq 
-by (auto simp add: permute_flip_at)
+lemma supp_finite_atom_set:
+  fixes S::"atom set"
+  assumes "finite S"
+  shows "supp S = S"
+  apply(rule finite_supp_unique)
+  apply(simp add: supports_def)
+  apply(simp add: swap_set_not_in)
+  apply(rule assms)
+  apply(simp add: swap_set_in)
+done
 
-lemma supp_finite:
-  fixes S::"'a::at set"
-  assumes asm: "finite S"
-  shows "(supp S) = atom ` S"
-sorry
 
+(*
 lemma supp_infinite:
   fixes S::"atom set"
   assumes asm: "finite (UNIV - S)"