diff -r 37285ec4387d -r e9e205b904e2 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Sun Dec 20 00:53:35 2009 +0100
+++ b/Quot/quotient_tacs.ML	Mon Dec 21 22:36:31 2009 +0100
@@ -389,7 +389,8 @@
 let
   val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt)
 in
-  inj_repabs_step_tac ctxt rel_refl
+  simp_tac ((mk_minimal_ss ctxt) addsimps (id_simps_get ctxt)) (* HACK? *) 
+  THEN' inj_repabs_step_tac ctxt rel_refl
 end
 
 fun all_inj_repabs_tac ctxt =
@@ -491,7 +492,7 @@
 (*                                                     *)
 (* 5. Test for refl                                    *)
 
-fun clean_tac lthy =
+fun clean_tac_aux lthy =
   let
     val thy = ProofContext.theory_of lthy;
     val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
@@ -508,7 +509,7 @@
             TRY o rtac refl]
   end
 
-
+fun clean_tac lthy = REPEAT o CHANGED o (clean_tac_aux lthy) (* HACK?? *)
 
 (* Tactic for Genralisation of Free Variables in a Goal *)