diff -r 0516a6c1ea59 -r 1a7ad2601cb5 src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Fri Mar 23 14:18:43 2012 +0100
+++ b/src/HOL/Library/Quotient_List.thy	Fri Mar 23 14:20:09 2012 +0100
@@ -8,8 +8,6 @@
 imports Main Quotient_Syntax
 begin
 
-declare [[map list = list_all2]]
-
 lemma map_id [id_simps]:
   "map id = id"
   by (fact List.map.id)
@@ -75,6 +73,8 @@
     by (induct xs ys rule: list_induct2') auto
 qed
 
+declare [[map list = (list_all2, list_quotient)]]
+
 lemma cons_prs [quot_preserve]:
   assumes q: "Quotient R Abs Rep"
   shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"