# HG changeset patch
# User wenzelm
# Date 935156091 -7200
# Node ID 43a0a5097701228eb1f110c63f2d123b49b0f64c
# Parent  6d43d525faccbcd25dec06314d79d00c16b21bfc
intro/elim: REPEAT1;

diff -r 6d43d525facc -r 43a0a5097701 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri Aug 20 11:54:32 1999 +0200
+++ b/src/Provers/classical.ML	Fri Aug 20 15:34:51 1999 +0200
@@ -1158,9 +1158,10 @@
 local
 
 fun intro_elim_tac netpair_of _ [] cs facts =
-      Method.same_tac facts THEN' FIRST' (map (biresolve_from_nets_tac o netpair_of) (get_nets cs))
+      Method.same_tac facts THEN'
+        (REPEAT1 o FIRST' (map (biresolve_from_nets_tac o netpair_of) (get_nets cs)))
   | intro_elim_tac _ res_tac rules _ facts =
-      Method.same_tac facts THEN' res_tac rules;
+      Method.same_tac facts THEN' (REPEAT1 o res_tac rules);
 
 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;