diff -r baff284c6fcc -r 4eca2c3e59f7 QuotMain.thy
--- 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}