src/HOL/MicroJava/BV/Effect.thy

   "xcpt_eff i G pc s et == 
    map (\<lambda>C. (the (match_exception_table G C pc et), case s of None \<Rightarrow> None | Some s' \<Rightarrow> Some ([Class C], snd s'))) 
        (xcpt_names (i,G,pc,et))"
 
   norm_eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> state_type option \<Rightarrow> state_type option"
-  "norm_eff i G == option_map (\<lambda>s. eff' (i,G,s))"
+  "norm_eff i G == Option.map (\<lambda>s. eff' (i,G,s))"
 
   eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> state_type option \<Rightarrow> succ_type"
   "eff i G pc et s == (map (\<lambda>pc'. (pc',norm_eff i G s)) (succs i pc)) @ (xcpt_eff i G pc s et)"
 
 constdefs