diff -r 3e7a6ec549d1 -r b91782991dc8 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Thu Jan 21 10:55:09 2010 +0100
+++ b/Quot/quotient_tacs.ML	Thu Jan 21 11:11:22 2010 +0100
@@ -500,7 +500,7 @@
 (* Cleaning consists of:
 
   1. folding of definitions and preservation lemmas;
-     and simplification with babs_prs all_prs ex_prs
+     and simplification with babs_prs all_prs ex_prs ex1_prs
 
   2. unfolding of ---> in front of everything, except
      bound variables
@@ -509,6 +509,7 @@
   3. simplification with lambda_prs
 
   4. simplification with Quotient_abs_rep Quotient_rel_rep id_simps
+     and ex1_prs (since it may need lambdas to be folded).
 
   5. test for refl 
 *)
@@ -520,8 +521,8 @@
   val ids = id_simps_get lthy
 
   fun mk_simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
-  val ss1 = mk_simps (defs @ prs @ @{thms babs_prs all_prs ex_prs})
-  val ss2 = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep} @ ids)
+  val ss1 = mk_simps (defs @ prs @ @{thms babs_prs all_prs ex_prs ex1_prs})
+  val ss2 = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep ex1_prs} @ ids)
 in
   EVERY' [simp_tac ss1,
           fun_map_tac lthy,