# HG changeset patch # User Cezary Kaliszyk # Date 1263294287 -3600 # Node ID 9531fafc0daa11b7efc3541bfc6343f765f4c9e7 # Parent d2fa1cf989319a7e1f9fc95b81a8a29d2b16c52d removed 3 hacks. diff -r d2fa1cf98931 -r 9531fafc0daa Quot/quotient_tacs.ML --- 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 *)