--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Mar 04 10:47:20 2009 +0100
@@ -553,7 +553,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))"
+ (Option.map (\<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")
@@ -675,7 +675,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 Option.map_def nth_append)
apply (case_tac "mt ! pc''")
apply simp+
done