src/HOL/Library/Quotient_Option.thy

--- a/src/HOL/Library/Quotient_Option.thy	Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Library/Quotient_Option.thy	Wed May 16 19:15:45 2012 +0200
@@ -46,7 +46,7 @@
 lemma split_option_ex: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))"
   by (metis option.exhaust) (* TODO: move to Option.thy *)
 
-lemma option_reflp:
+lemma option_reflp[reflp_preserve]:
   "reflp R \<Longrightarrow> reflp (option_rel R)"
   unfolding reflp_def split_option_all by simp