--- 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