--- a/Nominal-General/Nominal2_Atoms.thy	Wed Apr 28 07:27:28 2010 +0200
+++ b/Nominal-General/Nominal2_Atoms.thy	Wed Apr 28 08:22:20 2010 +0200
@@ -17,7 +17,6 @@
 *}
 
 lemma atom_image_cong:
-  fixes X Y::"('a::at_base) set"
   shows "(atom ` X = atom ` Y) = (X = Y)"
   apply(rule inj_image_eq_iff)
   apply(simp add: inj_on_def)
@@ -33,91 +32,22 @@
   done
 
 lemma supp_finite_at_set:
-  fixes S::"('a::at) set"
-  assumes a: "finite S"
-  shows "supp S = atom ` S"
-  apply(rule finite_supp_unique)
-  apply(simp add: supports_def)
-  apply(rule allI)+
-  apply(rule impI)
-  apply(rule swap_fresh_fresh)
-  apply(simp add: fresh_def)
-  apply(simp add: atom_image_supp)
-  apply(subst supp_finite_atom_set)
-  apply(rule finite_imageI)
-  apply(simp add: a)
-  apply(simp)
-  apply(simp add: fresh_def)
-  apply(simp add: atom_image_supp)
-  apply(subst supp_finite_atom_set)
-  apply(rule finite_imageI)
-  apply(simp add: a)
-  apply(simp)
-  apply(rule finite_imageI)
-  apply(simp add: a)
-  apply(drule swap_set_in)
-  apply(assumption)
-  apply(simp)
-  apply(simp add: image_eqvt)
-  apply(simp add: permute_fun_def)
-  apply(simp add: atom_eqvt)
-  apply(simp add: atom_image_cong)
-  done
-
-lemma supp_finite_at_set_aux:
-  fixes S::"('a::at) set"
   assumes a: "finite S"
   shows "supp S = atom ` S"
-proof
-  show "supp S \<subseteq> ((atom::'a::at \<Rightarrow> atom) ` S)" 
-    apply(rule supp_is_subset)
-    apply(simp add: supports_def)
-    apply(rule allI)+
-    apply(rule impI)
-    apply(rule swap_fresh_fresh)
-    apply(simp add: fresh_def)
-    apply(simp add: atom_image_supp)
-    apply(subst supp_finite_atom_set)
-    apply(rule finite_imageI)
-    apply(simp add: a)
-    apply(simp)
-    apply(simp add: fresh_def)
-    apply(simp add: atom_image_supp)
-    apply(subst supp_finite_atom_set)
-    apply(rule finite_imageI)
-    apply(simp add: a)
-    apply(simp)
-    apply(rule finite_imageI)
-    apply(simp add: a)
-    done
-next 
-  have "supp ((atom::'a::at \<Rightarrow> atom) ` S) \<subseteq> supp ((op `) (atom::'a::at \<Rightarrow> atom)) \<union> supp S"
-    by (simp add: supp_fun_app)
-  moreover
-  have "supp ((op `) (atom::'a::at \<Rightarrow> atom)) = {}"
-    apply(rule supp_fun_eqvt)
-    apply(perm_simp)
-    apply(simp)
-    done
-  moreover 
-  have "supp ((atom::'a::at \<Rightarrow> atom) ` S) = ((atom::'a::at \<Rightarrow> atom) ` S)" 
-    apply(subst supp_finite_atom_set)
-    apply(rule finite_imageI)
-    apply(simp add: a)
-    apply(simp)
-    done
-  ultimately 
-  show "((atom::'a::at \<Rightarrow> atom) ` S) \<subseteq> supp S" by simp
+proof -
+  have fin: "finite (atom ` S)" 
+    using a by (simp add: finite_imageI) 
+  have "supp S = supp (atom ` S)" by (rule atom_image_supp)
+  also have "\<dots> = atom ` S" using fin by (simp add: supp_finite_atom_set)
+  finally show "supp S = atom ` S" by simp
 qed
-  
 
 lemma supp_at_insert:
-  fixes S::"('a::at) set"
+  fixes a::"'a::at_base"
   assumes a: "finite S"
   shows "supp (insert a S) = supp a \<union> supp S"
   using a by (simp add: supp_finite_at_set supp_at_base)
 
-
 section {* A swapping operation for concrete atoms *}
   
 definition