# HG changeset patch
# User wenzelm
# Date 964691069 -7200
# Node ID 2f814053a6ccc60d930e839e0d3d44488c98b84a
# Parent  755330e55e18959f7345943f55d92ba0c1e30694
intro_elim_tac: bimatch_from;

diff -r 755330e55e18 -r 2f814053a6cc src/Provers/classical.ML
--- a/src/Provers/classical.ML	Wed Jul 26 19:43:28 2000 +0200
+++ b/src/Provers/classical.ML	Thu Jul 27 11:44:29 2000 +0200
@@ -1125,7 +1125,7 @@
 fun intro_elim_tac netpair_of res_tac rules cs facts =
   let
     val tac =
-      if null rules then FIRST' (map (biresolve_from_nets_tac o netpair_of) (get_nets cs))
+      if null rules then FIRST' (map (bimatch_from_nets_tac o netpair_of) (get_nets cs))
       else res_tac rules;
   in Method.insert_tac facts THEN' REPEAT_ALL_NEW tac end;