# 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;