# HG changeset patch
# User paulson
# Date 953547328 -3600
# Node ID 0be2c98f15a7161ed668806eb58231fabae1c38e
# Parent  209eb2db72e6cd964525938b4893470241aecd40
replaced best_tac by force_tac, allowing some arithmetic reasoning

diff -r 209eb2db72e6 -r 0be2c98f15a7 TFL/post.sml
--- a/TFL/post.sml	Mon Mar 20 10:32:02 2000 +0100
+++ b/TFL/post.sml	Mon Mar 20 11:15:28 2000 +0100
@@ -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 => best_tac
-			   (cs addSDs [not0_implies_Suc] addss ss)) 1),
+		  THEN TRY(CLASET' (fn cs => force_tac
+			   (cs addSDs [not0_implies_Suc], ss)) 1),
      simplifier = Rules.simpl_conv ss []};