--- a/Quot/QuotList.thy	Wed Dec 09 16:44:34 2009 +0100
+++ b/Quot/QuotList.thy	Wed Dec 09 17:05:33 2009 +0100
@@ -156,10 +156,7 @@
 apply simp_all
 done
 
-(* TODO: induct_tac doesn't accept 'arbitrary'.
-         induct     doesn't accept 'rule'.
-   that's why the proof uses manual generalisation and needs assumptions
-   both in conclusion for induction and in assumptions. *)
+(* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *)
 lemma foldl_rsp[quot_respect]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"