# 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 =