replaced best_tac by force_tac, allowing some arithmetic reasoning

--- 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 []};