
diff -r 3a1aef73b2b2 -r aea5d7fa7ef5 src/HOL/Import/HOL4Compat.thy
--- a/src/HOL/Import/HOL4Compat.thy	Wed Mar 04 11:05:02 2009 +0100
+++ b/src/HOL/Import/HOL4Compat.thy	Wed Mar 04 11:05:29 2009 +0100
@@ -73,7 +73,7 @@
 lemma option_case_def: "(!u f. option_case u f None = u) & (!u f x. option_case u f (Some x) = f x)"
   by simp
 
-lemma OPTION_MAP_DEF: "(!f x. option_map f (Some x) = Some (f x)) & (!f. option_map f None = None)"
+lemma OPTION_MAP_DEF: "(!f x. Option.map f (Some x) = Some (f x)) & (!f. Option.map f None = None)"
   by simp
 
 consts




