src/HOL/Lazy_Sequence.thy

   "list_of_lazy_sequence (map f xq) = List.map f (list_of_lazy_sequence xq)"
   by (simp add: map_def)
 
 lemma map_code [code]:
   "map f xq =
-    Lazy_Sequence (\<lambda>_. Option.map (\<lambda>(x, xq'). (f x, map f xq')) (yield xq))"
+    Lazy_Sequence (\<lambda>_. map_option (\<lambda>(x, xq'). (f x, map f xq')) (yield xq))"
   by (simp_all add: lazy_sequence_eq_iff split: list.splits)
 
 definition flat :: "'a lazy_sequence lazy_sequence \<Rightarrow> 'a lazy_sequence"
 where
   "flat xqq = lazy_sequence_of_list (concat (List.map list_of_lazy_sequence (list_of_lazy_sequence xqq)))"

 where
   "if_seq b = (if b then single () else empty)"
 
 definition those :: "'a option lazy_sequence \<Rightarrow> 'a lazy_sequence option"
 where
-  "those xq = Option.map lazy_sequence_of_list (List.those (list_of_lazy_sequence xq))"
+  "those xq = map_option lazy_sequence_of_list (List.those (list_of_lazy_sequence xq))"
   
 function iterate_upto :: "(natural \<Rightarrow> 'a) \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> 'a lazy_sequence"
 where
   "iterate_upto f n m =
     Lazy_Sequence (\<lambda>_. if n > m then None else Some (f n, iterate_upto f (n + 1) m))"

 where
   "hb_single x = Lazy_Sequence (\<lambda>_. Some (Some x, empty))"
 
 definition hb_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a hit_bound_lazy_sequence \<Rightarrow> 'b hit_bound_lazy_sequence"
 where
-  "hb_map f xq = map (Option.map f) xq"
+  "hb_map f xq = map (map_option f) xq"
 
 lemma hb_map_code [code]:
   "hb_map f xq =
-    Lazy_Sequence (\<lambda>_. Option.map (\<lambda>(x, xq'). (Option.map f x, hb_map f xq')) (yield xq))"
-  using map_code [of "Option.map f" xq] by (simp add: hb_map_def)
+    Lazy_Sequence (\<lambda>_. map_option (\<lambda>(x, xq'). (map_option f x, hb_map f xq')) (yield xq))"
+  using map_code [of "map_option f" xq] by (simp add: hb_map_def)
 
 definition hb_flat :: "'a hit_bound_lazy_sequence hit_bound_lazy_sequence \<Rightarrow> 'a hit_bound_lazy_sequence"
 where
   "hb_flat xqq = lazy_sequence_of_list (concat
-    (List.map ((\<lambda>x. case x of None \<Rightarrow> [None] | Some xs \<Rightarrow> xs) \<circ> Option.map list_of_lazy_sequence) (list_of_lazy_sequence xqq)))"
+    (List.map ((\<lambda>x. case x of None \<Rightarrow> [None] | Some xs \<Rightarrow> xs) \<circ> map_option list_of_lazy_sequence) (list_of_lazy_sequence xqq)))"
 
 lemma list_of_lazy_sequence_hb_flat [simp]:
   "list_of_lazy_sequence (hb_flat xqq) =
-    concat (List.map ((\<lambda>x. case x of None \<Rightarrow> [None] | Some xs \<Rightarrow> xs) \<circ> Option.map list_of_lazy_sequence) (list_of_lazy_sequence xqq))"
+    concat (List.map ((\<lambda>x. case x of None \<Rightarrow> [None] | Some xs \<Rightarrow> xs) \<circ> map_option list_of_lazy_sequence) (list_of_lazy_sequence xqq))"
   by (simp add: hb_flat_def)
 
 lemma hb_flat_code [code]:
   "hb_flat xqq = Lazy_Sequence (\<lambda>_. case yield xqq of
     None \<Rightarrow> None