--- 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"

--- a/Nominal/Nominal2_FSet.thy	Wed Apr 28 08:24:46 2010 +0200
+++ b/Nominal/Nominal2_FSet.thy	Wed Apr 28 08:32:33 2010 +0200
@@ -80,11 +80,11 @@
   done
 
 lemma supp_at_finsert:
-  fixes S::"('a::at) fset"
-  shows "supp (finsert x S) = supp x \<union> supp S"
+  fixes a::"'a::at_base"
+  shows "supp (finsert a S) = supp a \<union> supp S"
   apply (subst supp_fset_to_set[symmetric])
   apply (simp add: supp_finite_atom_set)
-  apply (simp add: supp_at_insert[OF fin_fset_to_set])
+  apply (simp add: supp_at_base_insert[OF fin_fset_to_set])
   apply (simp add: supp_fset_to_set)
   done
 
@@ -92,7 +92,7 @@
   "supp {||} = {}"
   by (simp add: supp_def eqvts)
 
-instance fset :: (at) fs
+instance fset :: (at_base) fs
   apply (default)
   apply (induct_tac x rule: fset_induct)
   apply (simp add: supp_fempty)
@@ -101,8 +101,9 @@
   done
 
 lemma supp_at_fset:
-  "supp (fset :: 'a :: at fset) = fset_to_set (fmap atom fset)"
-  apply (induct fset)
+  fixes S::"('a::at_base) fset"
+  shows "supp S = fset_to_set (fmap atom S)"
+  apply (induct S)
   apply (simp add: supp_fempty)
   apply (simp add: supp_at_finsert)
   apply (simp add: supp_at_base)