src/HOL/Option.thy

 lemma option_map_o_sum_case [simp]:
     "map f o sum_case g h = sum_case (map f o g) (map f o h)"
   by (rule ext) (simp split: sum.split)
 
 
-hide (open) const set map
+hide_const (open) set map
 
 subsubsection {* Code generator setup *}
 
 definition is_none :: "'a option \<Rightarrow> bool" where
   [code_post]: "is_none x \<longleftrightarrow> x = None"

 
 lemma [code_unfold]:
   "eq_class.eq x None \<longleftrightarrow> is_none x"
   by (simp add: eq is_none_none)
 
-hide (open) const is_none
+hide_const (open) is_none
 
 code_type option
   (SML "_ option")
   (OCaml "_ option")
   (Haskell "Maybe _")