# HG changeset patch
# User wenzelm
# Date 935487785 -7200
# Node ID 9053ad9a976848025ad55ba45d0c5979ff835639
# Parent  4265615b420687c91b494d6d15bcad4e11f1a6a0
fixed intro_elim_tac;

diff -r 4265615b4206 -r 9053ad9a9768 src/Provers/classical.ML
--- 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;