# HG changeset patch
# User lcp
# Date 784546385 -3600
# Node ID 98fc1a8e832a2bbfbfeea7ee9ed9d66a538b2904
# Parent  74ee8b9ff9a7c97a014c6c0bd64a745e64b24f36
FOL/intprover/safe_tac: now uses REPEAT_DETERM_FIRST instead of REPEAT_DETERM

diff -r 74ee8b9ff9a7 -r 98fc1a8e832a src/FOL/intprover.ML
--- a/src/FOL/intprover.ML	Fri Nov 11 10:31:51 1994 +0100
+++ b/src/FOL/intprover.ML	Fri Nov 11 10:33:05 1994 +0100
@@ -60,7 +60,7 @@
 			    bimatch_tac safep_brls] ;
 
 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
-val safe_tac = DETERM (REPEAT_FIRST safe_step_tac);
+val safe_tac = REPEAT_DETERM_FIRST safe_step_tac;
 
 (*These steps could instantiate variables and are therefore unsafe.*)
 val inst_step_tac =