diff -r bc9ed52bcef5 -r b41de1879dae Nominal/Abs.thy
--- a/Nominal/Abs.thy	Thu Mar 11 19:41:11 2010 +0100
+++ b/Nominal/Abs.thy	Thu Mar 11 19:43:50 2010 +0100
@@ -725,8 +725,6 @@
 
 (* support of concrete atom sets *)
 
-atom_decl name
-
 lemma atom_eqvt_raw:
   fixes p::"perm"
   shows "(p \<bullet> atom) = atom"
@@ -739,7 +737,7 @@
 done
 
 lemma
-  fixes as::"name set"
+  fixes as::"'a::at_base set"
   shows "supp (atom ` as) = supp as"
 apply(simp add: supp_def)
 apply(simp add: image_eqvt)