diff -r 024cf0f7fb6d -r f29e7dcd7c40 src/HOL/Library/Quotient_Option.thy
--- a/src/HOL/Library/Quotient_Option.thy	Thu Apr 26 01:05:06 2012 +0200
+++ b/src/HOL/Library/Quotient_Option.thy	Thu Apr 26 12:01:58 2012 +0200
@@ -101,15 +101,13 @@
 
 subsection {* Setup for lifting package *}
 
-lemma Quotient_option:
+lemma Quotient_option[quot_map]:
   assumes "Quotient R Abs Rep T"
   shows "Quotient (option_rel R) (Option.map Abs)
     (Option.map Rep) (option_rel T)"
   using assms unfolding Quotient_alt_def option_rel_unfold
   by (simp split: option.split)
 
-declare [[map option = (option_rel, Quotient_option)]]
-
 fun option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool"
 where
   "option_pred R None = True"