# HG changeset patch
# User paulson
# Date 892208429 -7200
# Node ID 20d292c05e6c455b2c6193e4b5a00a734e493060
# Parent  02b7c759159be11248eba779097dee04780e5a5c
can prove the empty relation to be WF

diff -r 02b7c759159b -r 20d292c05e6c TFL/post.sml
--- 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),