diff -r 6cc897e2468a -r 564117b58d73 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Jul 01 06:21:28 2008 +0200
+++ b/src/HOL/Set.thy	Tue Jul 01 06:51:59 2008 +0200
@@ -1324,7 +1324,7 @@
 lemma full_SetCompr_eq [noatp]: "{u. \<exists>x. u = f x} = range f"
   by auto
 
-lemma range_composition [simp]: "range (\<lambda>x. f (g x)) = f`range g"
+lemma range_composition: "range (\<lambda>x. f (g x)) = f`range g"
 by (subst image_image, simp)