diff -r 0516a6c1ea59 -r 1a7ad2601cb5 src/HOL/Library/Quotient_Option.thy
--- a/src/HOL/Library/Quotient_Option.thy	Fri Mar 23 14:18:43 2012 +0100
+++ b/src/HOL/Library/Quotient_Option.thy	Fri Mar 23 14:20:09 2012 +0100
@@ -16,8 +16,6 @@
 | "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
@@ -65,6 +63,8 @@
   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"