src/HOL/Library/Mapping.thy

     (\<lambda>k m. m(k := None)) (\<lambda>k m. m(k := None))"
   by transfer_prover
 
 lemma is_none_parametric [transfer_rule]:
   "(rel_option A ===> HOL.eq) Option.is_none Option.is_none"
-  by (auto simp add: is_none_def rel_fun_def rel_option_iff split: option.split)
+  by (auto simp add: Option.is_none_def rel_fun_def rel_option_iff split: option.split)
 
 lemma dom_parametric:
   assumes [transfer_rule]: "bi_total A"
   shows "((A ===> rel_option B) ===> rel_set A) dom dom" 
-  unfolding dom_def [abs_def] is_none_def [symmetric] by transfer_prover
+  unfolding dom_def [abs_def] Option.is_none_def [symmetric] by transfer_prover
 
 lemma map_of_parametric [transfer_rule]:
   assumes [transfer_rule]: "bi_unique R1"
   shows "(list_all2 (rel_prod R1 R2) ===> R1 ===> rel_option R2) map_of map_of"
   unfolding map_of_def by transfer_prover

   "lookup empty k = None" 
   by transfer simp
 
 lemma keys_is_none_rep [code_unfold]:
   "k \<in> keys m \<longleftrightarrow> \<not> (Option.is_none (lookup m k))"
-  by transfer (auto simp add: is_none_def)
+  by transfer (auto simp add: Option.is_none_def)
 
 lemma update_update:
   "update k v (update k w m) = update k v m"
   "k \<noteq> l \<Longrightarrow> update k v (update l w m) = update l w (update k v m)"
   by (transfer, simp add: fun_upd_twist)+