# HG changeset patch
# User haftmann
# Date 1174301975 -3600
# Node ID 01751f5b06578955d8072adceadc147afcc1fdcf
# Parent  c9357ef0116837e3b3f3eda5f08fed8fab6dc8f6
moved Output.overwrite_warn here

diff -r c9357ef01168 -r 01751f5b0657 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sun Mar 18 01:50:05 2007 +0100
+++ b/src/Provers/classical.ML	Mon Mar 19 11:59:35 2007 +0100
@@ -602,16 +602,23 @@
     safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
     haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
 
+fun overwrite_warn msg (p as (key : string, v)) xs =
+  let
+    fun over ((q as (keyi, _)) :: xs) =
+          if keyi = key then p :: xs else q :: over xs
+      | over [] = [p];
+  in (
+    if AList.defined (op =) xs key then () else warning msg;
+    over xs
+  ) end;
 
 (*Add/replace a safe wrapper*)
-fun cs addSWrapper new_swrapper = update_swrappers cs (fn swrappers =>
-    overwrite_warn (swrappers, new_swrapper)
-       ("Overwriting safe wrapper " ^ fst new_swrapper));
+fun cs addSWrapper new_swrapper = update_swrappers cs
+  (overwrite_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper);
 
 (*Add/replace an unsafe wrapper*)
-fun cs addWrapper new_uwrapper = update_uwrappers cs (fn uwrappers =>
-    overwrite_warn (uwrappers, new_uwrapper)
-        ("Overwriting unsafe wrapper "^fst new_uwrapper));
+fun cs addWrapper new_uwrapper = update_uwrappers cs
+  (overwrite_warn ("Overwriting unsafe wrapper "^fst new_uwrapper) new_uwrapper);
 
 (*Remove a safe wrapper*)
 fun cs delSWrapper name = update_swrappers cs (fn swrappers =>