src/HOL/Library/Quotient_Set.thy

--- a/src/HOL/Library/Quotient_Set.thy	Fri Mar 23 14:18:43 2012 +0100
+++ b/src/HOL/Library/Quotient_Set.thy	Fri Mar 23 14:20:09 2012 +0100
@@ -26,6 +26,8 @@
     by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient_def])+
 qed
 
+declare [[map set = (set_rel, set_quotient)]]
+
 lemma empty_set_rsp[quot_respect]:
   "set_rel R {} {}"
   unfolding set_rel_def by simp