diff -r de76079f973a -r d41f77196338 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Thu Oct 29 23:49:55 2009 +0100
+++ b/src/Provers/classical.ML	Thu Oct 29 23:56:33 2009 +0100
@@ -198,10 +198,10 @@
 (*Uses introduction rules in the normal way, or on negated assumptions,
   trying rules in order. *)
 fun swap_res_tac rls =
-    let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls
+    let fun addrl rl brls = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls
     in  assume_tac      ORELSE'
         contr_tac       ORELSE'
-        biresolve_tac (List.foldr addrl [] rls)
+        biresolve_tac (fold_rev addrl rls [])
     end;
 
 (*Duplication of hazardous rules, for complete provers*)