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