# HG changeset patch
# User nipkow
# Date 964540075 -7200
# Node ID 13b10be222bfd19a41aa5f3e60297e7029a053a8
# Parent  3c2fc90d4e8af665247598a6444ec2537957a78a
Replaced force by fast because force may now take forever to fail
(due to a recend change of David's)

diff -r 3c2fc90d4e8a -r 13b10be222bf TFL/post.sml
--- 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 []};