src/Provers/classical.ML
changeset 33339 d41f77196338
parent 33317 b4534348b8fd
child 33369 470a7b233ee5
     1.1 --- a/src/Provers/classical.ML	Thu Oct 29 23:49:55 2009 +0100
     1.2 +++ b/src/Provers/classical.ML	Thu Oct 29 23:56:33 2009 +0100
     1.3 @@ -198,10 +198,10 @@
     1.4  (*Uses introduction rules in the normal way, or on negated assumptions,
     1.5    trying rules in order. *)
     1.6  fun swap_res_tac rls =
     1.7 -    let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls
     1.8 +    let fun addrl rl brls = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls
     1.9      in  assume_tac      ORELSE'
    1.10          contr_tac       ORELSE'
    1.11 -        biresolve_tac (List.foldr addrl [] rls)
    1.12 +        biresolve_tac (fold_rev addrl rls [])
    1.13      end;
    1.14  
    1.15  (*Duplication of hazardous rules, for complete provers*)