--- a/Nominal/Abs.thy	Fri Mar 19 10:24:49 2010 +0100
+++ b/Nominal/Abs.thy	Fri Mar 19 12:22:10 2010 +0100
@@ -749,17 +749,6 @@
 
 (* support of concrete atom sets *)
 
-lemma atom_eqvt_raw:
-  fixes p::"perm"
-  shows "(p \<bullet> atom) = atom"
-by (simp add: expand_fun_eq permute_fun_def atom_eqvt)
-
-lemma atom_image_cong:
-  shows "(atom ` X = atom ` Y) = (X = Y)"
-apply(rule inj_image_eq_iff)
-apply(simp add: inj_on_def)
-done
-
 lemma supp_atom_image:
   fixes as::"'a::at_base set"
   shows "supp (atom ` as) = supp as"