--- 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 #)"