author | lcp |
Fri, 11 Nov 1994 10:33:05 +0100 | |
changeset 702 | 98fc1a8e832a |
parent 701 | 74ee8b9ff9a7 |
child 703 | 3a5cd2883581 |
--- 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 =