diff -r 0d31c0546286 -r 786edc984c98 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -551,7 +551,7 @@
 
 lemma match_xctable_offset: "
   (match_exception_table G cn (pc + n) (offset_xctable n et)) =
-  (Option.map (\<lambda> pc'. pc' + n) (match_exception_table G cn pc et))"
+  (map_option (\<lambda> pc'. pc' + n) (match_exception_table G cn pc et))"
 apply (induct et)
 apply (simp add: offset_xctable_def)+
 apply (case_tac "match_exception_entry G cn pc a")
@@ -672,7 +672,7 @@
         in app_jumps_lem)
   apply (simp add: nth_append)+
     (* subgoal \<exists> st. mt ! pc'' = Some st *)
-  apply (simp add: norm_eff_def Option.map_def nth_append)
+  apply (simp add: norm_eff_def map_option_case nth_append)
   apply (case_tac "mt ! pc''")
 apply simp+
 done