--- a/QuotList.thy	Sat Dec 05 23:26:08 2009 +0100
+++ b/QuotList.thy	Sat Dec 05 23:35:09 2009 +0100
@@ -132,7 +132,7 @@
          induct     doesn't accept 'rule'.
    that's why the proof uses manual generalisation and needs assumptions
    both in conclusion for induction and in assumptions. *)
-lemma foldl_rsp[quotient_rsp]:
+lemma foldl_rsp:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl"