# HG changeset patch
# User wenzelm
# Date 968095113 -7200
# Node ID e4ad74159b433989f9fd67c0a544db66c049c6b1
# Parent  bf49c3796599aac5bc367bce2f517de0700438b7
tuned;

diff -r bf49c3796599 -r e4ad74159b43 src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Sep 04 21:18:28 2000 +0200
+++ b/src/Pure/library.ML	Mon Sep 04 21:18:33 2000 +0200
@@ -1209,9 +1209,9 @@
 
 (** misc **)
 
-fun overwrite_warn (args as (alist,(a,_))) text =
-  (if is_none(assoc(alist,a)) then () else warning text;
-   overwrite args);
+fun overwrite_warn (args as (alist, (a, _))) msg =
+ (if is_none (assoc (alist, a)) then () else warning msg;
+  overwrite args);
 
 (*use the keyfun to make a list of (x, key) pairs*)
 fun make_keylist (keyfun: 'a->'b) : 'a list -> ('a * 'b) list =