src/Provers/classical.ML
changeset 15574 b1d1b5bfc464
parent 15570 8d8c70b41bab
child 15703 727ef1b8b3ee
     1.1 --- a/src/Provers/classical.ML	Fri Mar 04 11:44:26 2005 +0100
     1.2 +++ b/src/Provers/classical.ML	Fri Mar 04 15:07:34 2005 +0100
     1.3 @@ -214,7 +214,7 @@
     1.4      let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls
     1.5      in  assume_tac      ORELSE'
     1.6          contr_tac       ORELSE'
     1.7 -        biresolve_tac (Library.foldr addrl (rls,[]))
     1.8 +        biresolve_tac (foldr addrl [] rls)
     1.9      end;
    1.10  
    1.11  (*Duplication of hazardous rules, for complete provers*)
    1.12 @@ -286,7 +286,7 @@
    1.13  fun rep_cs (CS args) = args;
    1.14  
    1.15  local
    1.16 -  fun wrap l tac = Library.foldr (fn ((name,tacf),w) => tacf w) (l, tac);
    1.17 +  fun wrap l tac = foldr (fn ((name,tacf),w) => tacf w) tac l;
    1.18  in
    1.19    fun appSWrappers (CS{swrappers,...}) = wrap swrappers;
    1.20    fun appWrappers  (CS{uwrappers,...}) = wrap uwrappers;
    1.21 @@ -316,7 +316,7 @@
    1.22  fun tag_brls' _ _ [] = []
    1.23    | tag_brls' w k (brl::brls) = ((w, k), brl) :: tag_brls' w (k + 1) brls;
    1.24  
    1.25 -fun insert_tagged_list kbrls netpr = Library.foldr Tactic.insert_tagged_brl (kbrls, netpr);
    1.26 +fun insert_tagged_list kbrls netpr = foldr Tactic.insert_tagged_brl netpr kbrls;
    1.27  
    1.28  (*Insert into netpair that already has nI intr rules and nE elim rules.
    1.29    Count the intr rules double (to account for swapify).  Negate to give the
    1.30 @@ -324,7 +324,7 @@
    1.31  fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules;
    1.32  fun insert' w (nI, nE) = insert_tagged_list o tag_brls' w (~(nI + nE)) o joinrules';
    1.33  
    1.34 -fun delete_tagged_list brls netpr = Library.foldr Tactic.delete_tagged_brl (brls, netpr);
    1.35 +fun delete_tagged_list brls netpr = foldr Tactic.delete_tagged_brl netpr brls;
    1.36  fun delete x = delete_tagged_list (joinrules x);
    1.37  fun delete' x = delete_tagged_list (joinrules' x);
    1.38