--- a/src/HOL/Option.thy Sun Nov 26 13:19:52 2017 +0100
+++ b/src/HOL/Option.thy Sun Nov 26 21:08:32 2017 +0100
@@ -109,7 +109,7 @@
by (simp add: map_option_case split: option.split)
lemma map_option_o_case_sum [simp]:
- "map_option f o case_sum g h = case_sum (map_option f o g) (map_option f o h)"
+ "map_option f \<circ> case_sum g h = case_sum (map_option f \<circ> g) (map_option f \<circ> h)"
by (rule o_case_sum)
lemma map_option_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> map_option f x = map_option g y"