src/FOL/intprover.ML
changeset 702 98fc1a8e832a
parent 0 a5a9c433f639
child 1005 65188e520024
--- 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 =