diff -r ff7e6751a1a7 -r 9bbd5497befd src/HOL/Option.thy --- a/src/HOL/Option.thy Sat Nov 10 07:57:18 2018 +0000 +++ b/src/HOL/Option.thy Sat Nov 10 07:57:19 2018 +0000 @@ -260,7 +260,7 @@ lemma bind_map_option: "bind (map_option f x) g = bind x (g \ f)" by(cases x) simp_all -lemma set_bind_option [simp]: "set_option (bind x f) = UNION (set_option x) (set_option \ f)" +lemma set_bind_option [simp]: "set_option (bind x f) = (\((set_option \ f) ` set_option x))" by(cases x) auto lemma map_conv_bind_option: "map_option f x = Option.bind x (Some \ f)"