--- a/Quot/quotient_tacs.ML	Tue Jan 12 11:25:38 2010 +0100
+++ b/Quot/quotient_tacs.ML	Tue Jan 12 12:04:47 2010 +0100
@@ -158,7 +158,7 @@
   val bex_pat  = @{term "Bex (Respects (R1 ===> R2)) P"}
   val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc))
   val simpset = (mk_minimal_ss ctxt) 
-                       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} @ (id_simps_get ctxt)
+                       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
                        addsimprocs [simproc] 
                        addSolver equiv_solver addSolver quotient_solver
   val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt)
@@ -404,8 +404,7 @@
 let
   val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt)
 in
-  simp_tac ((mk_minimal_ss ctxt) addsimps (id_simps_get ctxt)) (* HACK? *) 
-  THEN' injection_step_tac ctxt rel_refl
+  injection_step_tac ctxt rel_refl
 end
 
 fun all_injection_tac ctxt =
@@ -511,7 +510,7 @@
 (*                                                     *)
 (* 5. test for refl                                    *)
 
-fun clean_tac_aux lthy =
+fun clean_tac lthy =
 let
   (* FIXME/TODO produce defs with lthy, like prs and ids *)
   val thy = ProofContext.theory_of lthy;
@@ -531,8 +530,6 @@
           TRY o rtac refl]  
 end
 
-fun clean_tac lthy = REPEAT o CHANGED o (clean_tac_aux lthy) (* HACK?? *)
-
 
 (****************************************************)
 (* Tactic for Generalising Free Variables in a Goal *)