1.1 --- a/src/HOL/Complete_Lattice.thy	Thu Jul 21 22:47:13 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Fri Jul 22 07:33:29 2011 +0200
     1.3 @@ -941,7 +941,7 @@
     1.4  lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})"
     1.5    by (fact SUP_eq)
     1.6  
     1.7 -lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)" -- "FIXME generalize"
     1.8 +lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
     1.9    by blast
    1.10  
    1.11  lemma UNION_empty_conv[simp]: