FOL/intprover/safe_tac: now uses REPEAT_DETERM_FIRST instead of REPEAT_DETERM
authorlcp
Fri, 11 Nov 1994 10:33:05 +0100
changeset 702 98fc1a8e832a
parent 701 74ee8b9ff9a7
child 703 3a5cd2883581
FOL/intprover/safe_tac: now uses REPEAT_DETERM_FIRST instead of REPEAT_DETERM
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 =