--- 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"