# HG changeset patch
# User wenzelm
# Date 955630842 -7200
# Node ID f93e2dbab86269732790e244af9a87a520433876
# Parent  8812dad6ef12e14d32e23a0b20c2d867f1124109
intro/elim_tac: match only;

diff -r 8812dad6ef12 -r f93e2dbab862 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Thu Apr 13 10:30:28 2000 +0200
+++ b/src/Provers/classical.ML	Thu Apr 13 15:00:42 2000 +0200
@@ -1119,8 +1119,8 @@
       else res_tac rules;
   in Method.insert_tac facts THEN' REPEAT_ALL_NEW tac end;
 
-val intro_tac = intro_elim_tac (fn (inet, _) => (inet, Net.empty)) resolve_tac;
-val elim_tac = intro_elim_tac (fn (_, enet) => (Net.empty, enet)) eresolve_tac;
+val intro_tac = intro_elim_tac (fn (inet, _) => (inet, Net.empty)) Tactic.match_tac;
+val elim_tac = intro_elim_tac (fn (_, enet) => (Net.empty, enet)) Tactic.ematch_tac;
 
 in
   val intro = METHOD_CLASET' o intro_tac;