src/HOL/List.thy

--- a/src/HOL/List.thy	Fri Feb 14 07:53:45 2014 +0100
+++ b/src/HOL/List.thy	Fri Feb 14 07:53:46 2014 +0100
@@ -182,7 +182,7 @@
 "those [] = Some []" |
 "those (x # xs) = (case x of
   None \<Rightarrow> None
-| Some y \<Rightarrow> Option.map (Cons y) (those xs))"
+| Some y \<Rightarrow> map_option (Cons y) (those xs))"
 
 primrec remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
 "remove1 x [] = []" |