# HG changeset patch # User wenzelm # Date 878557008 -3600 # Node ID ddd1c18121e04ba8616bd809aaa08107b6ac82ba # Parent 8cdf672a83e8fdc55b796dbb613d3d893ff8f755 CLASET'; diff -r 8cdf672a83e8 -r ddd1c18121e0 TFL/post.sml --- 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 []};