changeset 4097 | ddd1c18121e0 |
parent 3978 | 7e1cfed19d94 |
child 4805 | 20d292c05e6c |
--- a/TFL/post.sml Mon Nov 03 12:28:45 1997 +0100 +++ b/TFL/post.sml Mon Nov 03 12:36:48 1997 +0100 @@ -72,8 +72,8 @@ {WFtac = REPEAT (ares_tac [wf_measure, wf_inv_image, wf_lex_prod, wf_less_than, wf_trancl] 1), terminator = asm_simp_tac ss 1 - THEN TRY(best_tac - (!claset addSDs [not0_implies_Suc] addss ss) 1), + THEN TRY(CLASET' (fn cs => best_tac + (cs addSDs [not0_implies_Suc] addss ss)) 1), simplifier = Rules.simpl_conv ss []};