1.1 --- a/src/Provers/clasimp.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/Provers/clasimp.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -151,30 +151,30 @@
     1.4  in
     1.5  
     1.6  val op addIffs =
     1.7 -  foldl (addIff (Classical.addSDs, Classical.addSEs, Classical.addSIs)
     1.8 +  Library.foldl (addIff (Classical.addSDs, Classical.addSEs, Classical.addSIs)
     1.9      (Classical.addDs, Classical.addEs, Classical.addIs) Simplifier.addsimps);
    1.10 -val op delIffs = foldl (delIff Classical.delrules Simplifier.delsimps);
    1.11 +val op delIffs = Library.foldl (delIff Classical.delrules Simplifier.delsimps);
    1.12  
    1.13  fun AddIffs thms = store_clasimp (clasimpset () addIffs thms);
    1.14  fun DelIffs thms = store_clasimp (clasimpset () delIffs thms);
    1.15  
    1.16  fun addIffs_global (thy, ths) =
    1.17 -  foldl (addIff
    1.18 +  Library.foldl (addIff
    1.19      (ContextRules.addXDs_global, ContextRules.addXEs_global, ContextRules.addXIs_global)
    1.20      (ContextRules.addXDs_global, ContextRules.addXEs_global, ContextRules.addXIs_global) #1)
    1.21    ((thy, ()), ths) |> #1;
    1.22  
    1.23  fun addIffs_local (ctxt, ths) =
    1.24 -  foldl (addIff
    1.25 +  Library.foldl (addIff
    1.26      (ContextRules.addXDs_local, ContextRules.addXEs_local, ContextRules.addXIs_local)
    1.27      (ContextRules.addXDs_local, ContextRules.addXEs_local, ContextRules.addXIs_local) #1)
    1.28    ((ctxt, ()), ths) |> #1;
    1.29  
    1.30  fun delIffs_global (thy, ths) =
    1.31 -  foldl (delIff ContextRules.delrules_global #1) ((thy, ()), ths) |> #1;
    1.32 +  Library.foldl (delIff ContextRules.delrules_global #1) ((thy, ()), ths) |> #1;
    1.33  
    1.34  fun delIffs_local (ctxt, ths) =
    1.35 -  foldl (delIff ContextRules.delrules_local #1) ((ctxt, ()), ths) |> #1;
    1.36 +  Library.foldl (delIff ContextRules.delrules_local #1) ((ctxt, ()), ths) |> #1;
    1.37  
    1.38  end;
    1.39