src/HOL/Option.thy
changeset 55467 a5c9002bc54d
parent 55466 786edc984c98
child 55518 1ddb2edf5ceb
     1.1 --- a/src/HOL/Option.thy	Fri Feb 14 07:53:46 2014 +0100
     1.2 +++ b/src/HOL/Option.thy	Fri Feb 14 07:53:46 2014 +0100
     1.3 @@ -98,7 +98,7 @@
     1.4  lemma map_option_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> map_option f x = map_option g y"
     1.5  by (cases x) auto
     1.6  
     1.7 -enriched_type map_option: map_option proof -
     1.8 +functor map_option: map_option proof -
     1.9    fix f g
    1.10    show "map_option f \<circ> map_option g = map_option (f \<circ> g)"
    1.11    proof