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

--- a/QuotMain.thy	Sat Dec 05 23:26:08 2009 +0100
+++ b/QuotMain.thy	Sat Dec 05 23:35:09 2009 +0100
@@ -149,7 +149,7 @@
   fun_quotient list_quotient
 
 lemmas [quotient_rsp] =
-  quot_rel_rsp nil_rsp cons_rsp
+  quot_rel_rsp nil_rsp cons_rsp foldl_rsp
 
 ML {* maps_lookup @{theory} "List.list" *}
 ML {* maps_lookup @{theory} "*" *}
@@ -1104,7 +1104,7 @@
 fun clean_tac lthy =
   let
     val thy = ProofContext.theory_of lthy;
-    val defs = map (Thm.varifyT o #def) (qconsts_dest thy)
+    val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
     val thms1 = @{thms all_prs ex_prs}
     val thms2 = @{thms eq_reflection[OF fun_map.simps]} 
                 @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep}