diff -r ce774af6b964 -r a792bfc1be2b Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Tue Jan 26 12:24:23 2010 +0100
+++ b/Quot/quotient_tacs.ML	Tue Jan 26 13:38:42 2010 +0100
@@ -503,19 +503,17 @@
 
 (* Cleaning consists of:
 
-  1. folding of definitions and preservation lemmas;
-     and simplification with babs_prs all_prs ex_prs ex1_prs
-
-  2. unfolding of ---> in front of everything, except
+  1. unfolding of ---> in front of everything, except
      bound variables
      (this prevents lambda_prs from becoming stuck)
 
-  3. simplification with lambda_prs
+  2. 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).
+  3. simplification with Quotient_abs_rep Quotient_rel_rep id_simps
+     folding of definitions and preservation lemmas;
+     and simplification with babs_prs all_prs ex_prs ex1_prs
 
-  5. test for refl 
+  4. test for refl
 *)
 fun clean_tac lthy =
 let
@@ -525,13 +523,11 @@
   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 ex1_prs})
-  val ss2 = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep ex1_prs} @ ids)
+  val ss = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs)
 in
-  EVERY' [simp_tac ss1,
-          fun_map_tac lthy,
+  EVERY' [fun_map_tac lthy,
           lambda_prs_tac lthy,
-          simp_tac ss2,
+          simp_tac ss,
           TRY o rtac refl]
 end