--- a/Nominal/Nominal2_Base.thy	Tue Mar 08 09:07:49 2011 +0000
+++ b/Nominal/Nominal2_Base.thy	Fri Mar 11 08:51:39 2011 +0000
@@ -34,7 +34,7 @@
 primrec
   sort_of :: "atom \<Rightarrow> atom_sort"
 where
-  "sort_of (Atom s i) = s"
+  "sort_of (Atom s n) = s"
 
 primrec
   nat_of :: "atom \<Rightarrow> nat"
@@ -1121,9 +1121,7 @@
 lemma supp_eqvt [eqvt]:
   shows "p \<bullet> (supp x) = supp (p \<bullet> x)"
   unfolding supp_conv_fresh
-  unfolding Collect_def
-  unfolding permute_fun_def
-  by (simp add: Not_eqvt fresh_eqvt)
+  by (perm_simp) (rule refl)
 
 lemma fresh_permute_left:
   shows "a \<sharp> p \<bullet> x \<longleftrightarrow> - p \<bullet> a \<sharp> x"
@@ -1720,6 +1718,18 @@
   apply(simp add: swap_set_in)
 done
 
+lemma supp_cofinite_atom_set:
+  fixes S::"atom set"
+  assumes "finite (UNIV - S)"
+  shows "supp S = (UNIV - S)"
+  apply(rule finite_supp_unique)
+  apply(simp add: supports_def)
+  apply(simp add: swap_set_both_in)
+  apply(rule assms)
+  apply(subst swap_commute)
+  apply(simp add: swap_set_in)
+done
+
 lemma fresh_finite_atom_set:
   fixes S::"atom set"
   assumes "finite S"