# HG changeset patch
# User wenzelm
# Date 931861942 -7200
# Node ID f22a51ed9f11d673997647808b50ff38a83e1d31
# Parent  efb605156ca3cb3dfeda4bb3257532836b087d60
same_tac;

diff -r efb605156ca3 -r f22a51ed9f11 src/Provers/simplifier.ML
--- 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;