# HG changeset patch
# User lcp
# Date 750675870 -3600
# Node ID 3dea30013b58cd61592382d7a34a1419837d0a40
# Parent  f8f37a9a31dcbd18bcd5d3680254ab07a7bb312e
classical/swap_res_tac: recoded to allow backtracking

diff -r f8f37a9a31dc -r 3dea30013b58 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Oct 12 13:39:35 1993 +0100
+++ b/src/Provers/classical.ML	Fri Oct 15 10:04:30 1993 +0100
@@ -83,8 +83,10 @@
 (*Uses introduction rules in the normal way, or on negated assumptions,
   trying rules in order. *)
 fun swap_res_tac rls = 
-    let fun tacf rl = rtac rl ORELSE' etac (rl RSN (2,swap))
-    in  assume_tac ORELSE' contr_tac ORELSE' FIRST' (map tacf rls)
+    let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls
+    in  assume_tac 	ORELSE' 
+	contr_tac 	ORELSE' 
+        biresolve_tac (foldr addrl (rls,[]))
     end;
 
 (*Given assumption P-->Q, reduces subgoal Q to P [deletes the implication!] *)