--- a/Quot/Nominal/Nominal2_Supp.thy	Mon Feb 01 15:57:37 2010 +0100
+++ b/Quot/Nominal/Nominal2_Supp.thy	Mon Feb 01 16:13:24 2010 +0100
@@ -345,23 +345,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(auto simp add: permute_set_eq_vimage vimage_def swap_atom)[1]
+  apply(rule assms)
+  apply(auto simp add: permute_set_eq swap_atom)[1]
+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)"