--- a/Quot/QuotList.thy	Tue Dec 08 12:36:28 2009 +0100
+++ b/Quot/QuotList.thy	Tue Dec 08 12:59:38 2009 +0100
@@ -93,7 +93,7 @@
   shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l"
 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
 
-lemma map_rsp:
+lemma map_rsp[quotient_rsp]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map"
@@ -105,16 +105,6 @@
 apply simp_all
 done
 
-(* TODO: if the above is correct, we can remove this one *)
-lemma map_rsp_lo:
-  assumes q1: "Quotient R1 Abs1 Rep1"
-  and     q2: "Quotient R2 Abs2 Rep2"
-  and     a: "(R1 ===> R2) f1 f2"
-  and     b: "list_rel R1 l1 l2"
-  shows "list_rel R2 (map f1 l1) (map f2 l2)"
-using b a
-by (induct l1 l2 rule: list_induct2') (simp_all)
-
 lemma foldr_prs:
   assumes a: "Quotient R1 abs1 rep1"
   and     b: "Quotient R2 abs2 rep2"