changeset 8526 | 0be2c98f15a7 |
parent 7262 | a05dc63ca29b |
child 8622 | 870a58dd0ddd |
--- a/TFL/post.sml Mon Mar 20 10:32:02 2000 +0100 +++ b/TFL/post.sml Mon Mar 20 11:15:28 2000 +0100 @@ -92,8 +92,8 @@ wf_measure, wf_inv_image, wf_lex_prod, wf_less_than, wf_trancl] 1), terminator = asm_simp_tac ss 1 - THEN TRY(CLASET' (fn cs => best_tac - (cs addSDs [not0_implies_Suc] addss ss)) 1), + THEN TRY(CLASET' (fn cs => force_tac + (cs addSDs [not0_implies_Suc], ss)) 1), simplifier = Rules.simpl_conv ss []};