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;