--- a/Nominal-General/Nominal2_Base.thy	Wed Apr 28 08:24:46 2010 +0200
+++ b/Nominal-General/Nominal2_Base.thy	Wed Apr 28 08:32:33 2010 +0200
@@ -1188,7 +1188,7 @@
   apply(simp add: atom_image_cong)
   done
 
-lemma supp_finite_at_set:
+lemma supp_finite_set_at_base:
   assumes a: "finite S"
   shows "supp S = atom ` S"
 proof -
@@ -1199,11 +1199,11 @@
   finally show "supp S = atom ` S" by simp
 qed
 
-lemma supp_at_insert:
+lemma supp_at_base_insert:
   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)
+  using a by (simp add: supp_finite_set_at_base supp_at_base)
 
 section {* library functions for the nominal infrastructure *}
 use "nominal_library.ML"