diff -r 79136ce06bdb -r 58d147683393 src/HOL/MicroJava/BV/Opt.thy
--- a/src/HOL/MicroJava/BV/Opt.thy	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/MicroJava/BV/Opt.thy	Wed Mar 04 10:47:20 2009 +0100
@@ -286,8 +286,8 @@
 
 lemma option_map_in_optionI:
   "\<lbrakk> ox : opt S; !x:S. ox = Some x \<longrightarrow> f x : S \<rbrakk> 
-  \<Longrightarrow> option_map f ox : opt S";
-apply (unfold option_map_def)
+  \<Longrightarrow> Option.map f ox : opt S";
+apply (unfold Option.map_def)
 apply (simp split: option.split)
 apply blast
 done