# HG changeset patch
# User wenzelm
# Date 1330351219 -3600
# Node ID f800eb467515e6e903a40f2916b75b2fac3c883d
# Parent  b103fffd587fc3867a1aa0ffdafb2736b425d6de
simplified cut_tac (cf. d549b5b0f344);

diff -r b103fffd587f -r f800eb467515 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Mon Feb 27 14:07:59 2012 +0100
+++ b/src/Pure/tactic.ML	Mon Feb 27 15:00:19 2012 +0100
@@ -31,7 +31,7 @@
   val flexflex_tac: tactic
   val distinct_subgoal_tac: int -> tactic
   val distinct_subgoals_tac: tactic
-  val metacut_tac: thm -> int -> tactic
+  val cut_tac: thm -> int -> tactic
   val cut_rules_tac: thm list -> int -> tactic
   val cut_facts_tac: thm list -> int -> tactic
   val filter_thms: (term * term -> bool) -> int * term * thm list -> thm list
@@ -181,11 +181,11 @@
 
 (*The conclusion of the rule gets assumed in subgoal i,
   while subgoal i+1,... are the premises of the rule.*)
-fun metacut_tac rule i = resolve_tac [cut_rl] i  THEN  biresolve_tac [(false, rule)] (i+1);
+fun cut_tac rule i = rtac cut_rl i THEN rtac rule (i + 1);
 
 (*"Cut" a list of rules into the goal.  Their premises will become new
   subgoals.*)
-fun cut_rules_tac ths i = EVERY (map (fn th => metacut_tac th i) ths);
+fun cut_rules_tac ths i = EVERY (map (fn th => cut_tac th i) ths);
 
 (*As above, but inserts only facts (unconditional theorems);
   generates no additional subgoals. *)