# HG changeset patch
# User haftmann
# Date 1174301976 -3600
# Node ID 365bce31e0519964ff6310aa618e9c24f0553f25
# Parent  01751f5b06578955d8072adceadc147afcc1fdcf
dropped overwrite_warn

diff -r 01751f5b0657 -r 365bce31e051 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Mar 19 11:59:35 2007 +0100
+++ b/src/Pure/General/output.ML	Mon Mar 19 11:59:36 2007 +0100
@@ -24,7 +24,6 @@
   val priority: string -> unit
   val tracing: string -> unit
   val warning: string -> unit
-  val overwrite_warn: (''a * 'b) list * (''a * 'b) -> string -> (''a * 'b) list
   val debugging: bool ref
   val no_warnings: ('a -> 'b) -> 'a -> 'b
   val timing: bool ref
@@ -151,19 +150,6 @@
 fun ML_errors f = setmp do_toplevel_errors true (toplevel_errors f);
 
 
-(* overwriting change with warning *)
-
-fun overwrite (al, p as (key, _)) =
-  let fun over ((q as (keyi, _)) :: pairs) =
-            if keyi = key then p :: pairs else q :: (over pairs)
-        | over [] = [p]
-  in over al end;
-
-fun overwrite_warn (args as (alist, (a, _))) msg =
- (if is_none (AList.lookup (op =) alist a) then () else warning msg;
-  overwrite args);
-
-
 (* add_mode *)
 
 fun add_mode name (output, keyword, indent, raw) =