--- a/src/HOL/MicroJava/BV/Effect.thy Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy Wed Mar 04 10:47:20 2009 +0100
@@ -105,7 +105,7 @@
(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)"