--- a/QuotMain.thy	Sun Dec 06 00:13:35 2009 +0100
+++ b/QuotMain.thy	Sun Dec 06 00:19:45 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} "*" *}
@@ -1110,11 +1110,10 @@
 fun clean_tac lthy =
   let
     val thy = ProofContext.theory_of lthy;
-    val defs = map (Thm.varifyT o #def) (qconsts_dest thy)
-    val thms1 = @{thms all_prs ex_prs}
+    val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
+    val thms1 = @{thms all_prs ex_prs} @ defs
     val thms2 = @{thms eq_reflection[OF fun_map.simps]} 
                 @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} 
-                @ defs
     fun simp_ctxt thms = HOL_basic_ss addsimps thms addSolver quotient_solver
     (* FIXME: use of someting smaller than HOL_basic_ss *)
   in