Replaced force by fast because force may now take forever to fail
(due to a recend change of David's)

--- a/TFL/post.sml	Tue Jul 25 09:48:39 2000 +0200
+++ b/TFL/post.sml	Tue Jul 25 17:47:55 2000 +0200
@@ -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 => force_tac
-			   (cs addSDs [not0_implies_Suc], ss)) 1),
+		  THEN TRY(CLASET' (fn cs => fast_tac
+			   (cs addSDs [not0_implies_Suc] addss ss)) 1),
      simplifier = Rules.simpl_conv ss []};