# HG changeset patch
# User wenzelm
# Date 931811119 -7200
# Node ID 4b9963810121f230178b6a54693a65e6f71f2d97
# Parent  a5b67157b94dc74bf3e98ecc81ebdd189f66e619
removed metacuts_tac;

diff -r a5b67157b94d -r 4b9963810121 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Mon Jul 12 22:23:59 1999 +0200
+++ b/src/Pure/tactic.ML	Mon Jul 12 22:25:19 1999 +0200
@@ -62,7 +62,6 @@
   val match_from_net_tac	: (int*thm) Net.net -> int -> tactic
   val match_tac	: thm list -> int -> tactic
   val metacut_tac	: thm -> int -> tactic
-  val metacuts_tac	: thm list -> int -> tactic   
   val net_bimatch_tac	: (bool*thm) list -> int -> tactic
   val net_biresolve_tac	: (bool*thm) list -> int -> tactic
   val net_match_tac	: thm list -> int -> tactic
@@ -326,7 +325,6 @@
 (*The conclusion of the rule gets assumed in subgoal i,
   while subgoal i+1,... are the premises of the rule.*)
 fun metacut_tac rule = bires_cut_tac [(false,rule)];
-fun metacuts_tac rules i = EVERY (map (fn th => metacut_tac th i) rules);
 
 (*Recognizes theorems that are not rules, but simple propositions*)
 fun is_fact rl =