changeset 6994 | f22a51ed9f11 |
parent 6911 | ef0f25d0bc2d |
child 7132 | 5c31d06ead04 |
--- a/src/Provers/simplifier.ML Tue Jul 13 10:45:47 1999 +0200 +++ b/src/Provers/simplifier.ML Tue Jul 13 12:32:22 1999 +0200 @@ -465,7 +465,7 @@ fun simp_meth thin cut tac ctxt = Method.METHOD (fn facts => FIRSTGOAL ((if thin then REPEAT_DETERM o etac Drule.thin_rl else K all_tac) - THEN' (if cut then metacuts_tac facts else K all_tac) + THEN' (if cut then Method.same_tac facts else K all_tac) THEN' tac (get_local_simpset ctxt))); val simp_method = simp_args ooo simp_meth;