src/HOL/Datatype.thy
changeset 28562 4e74209f113e
parent 28524 644b62cf678f
child 28689 2947dc320178
     1.1 --- a/src/HOL/Datatype.thy	Fri Oct 10 06:45:50 2008 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Fri Oct 10 06:45:53 2008 +0200
     1.3 @@ -635,7 +635,7 @@
     1.4  definition
     1.5    option_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"
     1.6  where
     1.7 -  [code func del]: "option_map = (%f y. case y of None => None | Some x => Some (f x))"
     1.8 +  [code del]: "option_map = (%f y. case y of None => None | Some x => Some (f x))"
     1.9  
    1.10  lemma option_map_None [simp, code]: "option_map f None = None"
    1.11    by (simp add: option_map_def)