# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1268333030 -3600
# Node ID b41de1879daef54039f0b11484e7a94647bff3cb
# Parent  bc9ed52bcef51d34ed20b63652ef6c18124225cc
generalised the supp for atoms to all concrete atoms (not just names)

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)