src/HOL/Library/Mapping.thy

   "\<lambda>f g m. (map_option g \<circ> m \<circ> f)" parametric map_transfer .
 
 
 subsection {* Functorial structure *}
 
-enriched_type map: map
+functor map: map
   by (transfer, auto simp add: fun_eq_iff option.map_comp option.map_id)+
 
 
 subsection {* Derived operations *}