src/HOL/Map.thy

--- a/src/HOL/Map.thy	Mon Apr 13 13:03:41 2015 +0200
+++ b/src/HOL/Map.thy	Tue Apr 14 11:32:01 2015 +0200
@@ -641,6 +641,8 @@
   ultimately show ?case by (simp only: map_of.simps ran_map_upd) simp
 qed
 
+lemma ran_map_option: "ran (\<lambda>x. map_option f (m x)) = f ` ran m"
+by(auto simp add: ran_def)
 
 subsection {* @{text "map_le"} *}