diff -r 0d31c0546286 -r 786edc984c98 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/Library/Mapping.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -65,7 +65,7 @@
 
 lemma map_transfer: 
   "((A ===> B) ===> (C ===> D) ===> (B ===> option_rel C) ===> A ===> option_rel D) 
-    (\<lambda>f g m. (Option.map g \<circ> m \<circ> f)) (\<lambda>f g m. (Option.map g \<circ> m \<circ> f))"
+    (\<lambda>f g m. (map_option g \<circ> m \<circ> f)) (\<lambda>f g m. (map_option g \<circ> m \<circ> f))"
 by transfer_prover
 
 lemma map_entry_transfer:
@@ -105,13 +105,13 @@
   "\<lambda>xs k. if k < length xs then Some (xs ! k) else None" parametric bulkload_transfer .
 
 lift_definition map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('c, 'd) mapping" is
-  "\<lambda>f g m. (Option.map g \<circ> m \<circ> f)" parametric map_transfer .
+  "\<lambda>f g m. (map_option g \<circ> m \<circ> f)" parametric map_transfer .
 
 
 subsection {* Functorial structure *}
 
 enriched_type map: map
-  by (transfer, auto simp add: fun_eq_iff Option.map.compositionality Option.map.id)+
+  by (transfer, auto simp add: fun_eq_iff option.map_comp option.map_id)+
 
 
 subsection {* Derived operations *}
@@ -367,5 +367,3 @@
   replace default map_entry map_default tabulate bulkload map of_alist
 
 end
-
-