src/Provers/classical.ML
changeset 22468 01751f5b0657
parent 22360 26ead7ed4f4b
child 22474 ecdaec8cf13a
     1.1 --- a/src/Provers/classical.ML	Sun Mar 18 01:50:05 2007 +0100
     1.2 +++ b/src/Provers/classical.ML	Mon Mar 19 11:59:35 2007 +0100
     1.3 @@ -602,16 +602,23 @@
     1.4      safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
     1.5      haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
     1.6  
     1.7 +fun overwrite_warn msg (p as (key : string, v)) xs =
     1.8 +  let
     1.9 +    fun over ((q as (keyi, _)) :: xs) =
    1.10 +          if keyi = key then p :: xs else q :: over xs
    1.11 +      | over [] = [p];
    1.12 +  in (
    1.13 +    if AList.defined (op =) xs key then () else warning msg;
    1.14 +    over xs
    1.15 +  ) end;
    1.16  
    1.17  (*Add/replace a safe wrapper*)
    1.18 -fun cs addSWrapper new_swrapper = update_swrappers cs (fn swrappers =>
    1.19 -    overwrite_warn (swrappers, new_swrapper)
    1.20 -       ("Overwriting safe wrapper " ^ fst new_swrapper));
    1.21 +fun cs addSWrapper new_swrapper = update_swrappers cs
    1.22 +  (overwrite_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper);
    1.23  
    1.24  (*Add/replace an unsafe wrapper*)
    1.25 -fun cs addWrapper new_uwrapper = update_uwrappers cs (fn uwrappers =>
    1.26 -    overwrite_warn (uwrappers, new_uwrapper)
    1.27 -        ("Overwriting unsafe wrapper "^fst new_uwrapper));
    1.28 +fun cs addWrapper new_uwrapper = update_uwrappers cs
    1.29 +  (overwrite_warn ("Overwriting unsafe wrapper "^fst new_uwrapper) new_uwrapper);
    1.30  
    1.31  (*Remove a safe wrapper*)
    1.32  fun cs delSWrapper name = update_swrappers cs (fn swrappers =>