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