fixed intro_elim_tac;

--- a/src/Provers/classical.ML	Mon Aug 23 16:58:00 1999 +0200
+++ b/src/Provers/classical.ML	Tue Aug 24 11:43:05 1999 +0200
@@ -1157,11 +1157,13 @@
 
 local
 
-fun intro_elim_tac netpair_of _ [] cs facts =
-      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' (REPEAT1 o res_tac rules);
+fun intro_elim_tac netpair_of res_tac rules cs facts =
+  let
+    val single_tac =
+      if null rules then FIRST' (map (biresolve_from_nets_tac o netpair_of) (get_nets cs))
+      else res_tac rules;
+    fun multi_tac st = (single_tac THEN_ALL_NEW (TRY o (fn st => multi_tac st))) st;
+  in Method.same_tac facts THEN' multi_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;