src/Provers/classical.ML
changeset 23178 07ba6b58b3d2
parent 22846 fb79144af9a3
child 23594 e65e466dda01
     1.1 --- a/src/Provers/classical.ML	Thu May 31 23:02:16 2007 +0200
     1.2 +++ b/src/Provers/classical.ML	Thu May 31 23:47:36 2007 +0200
     1.3 @@ -326,7 +326,7 @@
     1.4  fun tag_brls' _ _ [] = []
     1.5    | tag_brls' w k (brl::brls) = ((w, k), brl) :: tag_brls' w (k + 1) brls;
     1.6  
     1.7 -fun insert_tagged_list kbrls netpr = foldr Tactic.insert_tagged_brl netpr kbrls;
     1.8 +fun insert_tagged_list rls = fold_rev Tactic.insert_tagged_brl rls;
     1.9  
    1.10  (*Insert into netpair that already has nI intr rules and nE elim rules.
    1.11    Count the intr rules double (to account for swapify).  Negate to give the
    1.12 @@ -334,7 +334,7 @@
    1.13  fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules;
    1.14  fun insert' w (nI, nE) = insert_tagged_list o tag_brls' w (~(nI + nE)) o joinrules';
    1.15  
    1.16 -fun delete_tagged_list brls netpr = foldr Tactic.delete_tagged_brl netpr brls;
    1.17 +fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls;
    1.18  fun delete x = delete_tagged_list (joinrules x);
    1.19  fun delete' x = delete_tagged_list (joinrules' x);
    1.20