src/HOL/Library/Quotient_Option.thy

 where
   "option_rel R None None = True"
 | "option_rel R (Some x) None = False"
 | "option_rel R None (Some x) = False"
 | "option_rel R (Some x) (Some y) = R x y"
-
-declare [[map option = option_rel]]
 
 lemma option_rel_unfold:
   "option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True
     | (Some x, Some y) \<Rightarrow> R x y
     | _ \<Rightarrow> False)"

   apply (simp_all add: Option.map.compositionality comp_def Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient_abs_rep [OF assms] Quotient_rel_rep [OF assms])
   using Quotient_rel [OF assms]
   apply (simp add: option_rel_unfold split: option.split)
   done
 
+declare [[map option = (option_rel, option_quotient)]]
+
 lemma option_None_rsp [quot_respect]:
   assumes q: "Quotient R Abs Rep"
   shows "option_rel R None None"
   by simp