diff -r d66f25a206b4 -r 1c4754938980 src/HOL/Option.ML
--- a/src/HOL/Option.ML	Fri Jul 14 16:28:56 2000 +0200
+++ b/src/HOL/Option.ML	Fri Jul 14 16:28:58 2000 +0200
@@ -60,6 +60,13 @@
 qed "option_map_eq_Some";
 AddIffs[option_map_eq_Some];
 
+Goal 
+"option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)";
+by (rtac ext 1);
+by (simp_tac (simpset() addsplits [sum.split]) 1);
+qed "option_map_o_sum_case";
+Addsimps [option_map_o_sum_case];
+
 
 section "o2s";