--- a/TFL/post.sml Fri Apr 10 13:15:28 1998 +0200
+++ b/TFL/post.sml Fri Apr 10 13:40:29 1998 +0200
@@ -69,8 +69,8 @@
*--------------------------------------------------------------------------*)
fun std_postprocessor ss =
Prim.postprocess
- {WFtac = REPEAT (ares_tac [wf_measure, wf_inv_image, wf_lex_prod,
- wf_less_than, wf_trancl] 1),
+ {WFtac = REPEAT (ares_tac [wf_empty, 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),