--- a/QuotMain.thy	Wed Dec 02 14:37:21 2009 +0100
+++ b/QuotMain.thy	Wed Dec 02 17:15:36 2009 +0100
@@ -787,6 +787,7 @@
     [rtac @{thm FUN_QUOTIENT},
      resolve_tac quot_thms,
      rtac @{thm IDENTITY_QUOTIENT},
+     rtac @{thm LIST_QUOTIENT},
      (* For functional identity quotients, (op = ---> op =) *)
      (* TODO: think about the other way around, if we need to shorten the relation *)
      CHANGED o (simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms id_simps}))])
@@ -1222,7 +1223,7 @@
     val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps
       (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs)
   in
-    EVERY' [lambda_prs_tac lthy quot,
+    EVERY' [TRY o lambda_prs_tac lthy quot,
             TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),
             TRY o simp_tac simp_ctxt,
             TRY o rtac refl]