--- a/Nominal-General/Nominal2_Base.thy	Wed Apr 21 21:52:30 2010 +0200
+++ b/Nominal-General/Nominal2_Base.thy	Thu Apr 22 05:16:23 2010 +0200
@@ -809,22 +809,6 @@
   qed
 qed
 
-section {* Support for finite sets of atoms *}
-
-
-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
-
-
-
 section {* Finitely-supported types *}
 
 class fs = pt +
@@ -860,6 +844,24 @@
 instance atom :: fs
 by default (simp add: supp_atom)
 
+section {* Support for finite sets of atoms *}
+
+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_atom_insert:
+  fixes S::"atom set"
+  assumes a: "finite S"
+  shows "supp (insert a S) = supp a \<union> supp S"
+  using a by (simp add: supp_finite_atom_set supp_atom)
 
 section {* Type @{typ perm} is finitely-supported. *}