diff -r 0516a6c1ea59 -r 1a7ad2601cb5 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