--- a/src/HOL/Datatype.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Datatype.thy Fri Oct 10 06:45:53 2008 +0200
@@ -635,7 +635,7 @@
definition
option_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"
where
- [code func del]: "option_map = (%f y. case y of None => None | Some x => Some (f x))"
+ [code del]: "option_map = (%f y. case y of None => None | Some x => Some (f x))"
lemma option_map_None [simp, code]: "option_map f None = None"
by (simp add: option_map_def)