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 =