prefer direct rotate_prems over old-style COMP;
authorwenzelm
Mon, 25 Jun 2012 17:44:16 +0200
changeset 49141cdbdbfa6a29f
parent 49140 602dc0215954
child 49142 d30957198bbb
prefer direct rotate_prems over old-style COMP;
src/Provers/classical.ML
     1.1 --- a/src/Provers/classical.ML	Mon Jun 25 17:41:20 2012 +0200
     1.2 +++ b/src/Provers/classical.ML	Mon Jun 25 17:44:16 2012 +0200
     1.3 @@ -907,7 +907,7 @@
     1.4  
     1.5  (* contradiction method *)
     1.6  
     1.7 -val contradiction = Method.rule [Data.not_elim, Data.not_elim COMP Drule.swap_prems_rl];
     1.8 +val contradiction = Method.rule [Data.not_elim, Drule.rotate_prems 1 Data.not_elim];
     1.9  
    1.10  
    1.11  (* automatic methods *)