diff -r 066bb557570f -r 7619080e49f0 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Wed Aug 15 09:02:11 2007 +0200
+++ b/src/HOL/Fun.thy	Wed Aug 15 12:52:56 2007 +0200
@@ -268,7 +268,7 @@
 lemma vimage_id [simp]: "id -` A = A"
 by (simp add: id_def)
 
-lemma vimage_image_eq: "f -` (f ` A) = {y. EX x:A. f x = f y}"
+lemma vimage_image_eq [noatp]: "f -` (f ` A) = {y. EX x:A. f x = f y}"
 by (blast intro: sym)
 
 lemma image_vimage_subset: "f ` (f -` A) <= A"