diff -r 024cf0f7fb6d -r f29e7dcd7c40 src/HOL/Library/Quotient_Set.thy
--- a/src/HOL/Library/Quotient_Set.thy	Thu Apr 26 01:05:06 2012 +0200
+++ b/src/HOL/Library/Quotient_Set.thy	Thu Apr 26 12:01:58 2012 +0200
@@ -185,7 +185,7 @@
 
 subsection {* Setup for lifting package *}
 
-lemma Quotient_set:
+lemma Quotient_set[quot_map]:
   assumes "Quotient R Abs Rep T"
   shows "Quotient (set_rel R) (image Abs) (image Rep) (set_rel T)"
   using assms unfolding Quotient_alt_def4
@@ -193,8 +193,6 @@
   apply (simp add: set_rel_def, fast)
   done
 
-declare [[map set = (set_rel, Quotient_set)]]
-
 lemma set_invariant_commute [invariant_commute]:
   "set_rel (Lifting.invariant P) = Lifting.invariant (\<lambda>A. Ball A P)"
   unfolding fun_eq_iff set_rel_def Lifting.invariant_def Ball_def by fast