src/Pure/General/output.ML
changeset 17521 0f1c48de39f5
parent 17412 e26cb20ef0cc
child 17539 b2ce48df4d4c
     1.1 --- a/src/Pure/General/output.ML	Tue Sep 20 15:12:40 2005 +0200
     1.2 +++ b/src/Pure/General/output.ML	Tue Sep 20 16:17:34 2005 +0200
     1.3 @@ -160,10 +160,13 @@
     1.4    in asl l end;
     1.5  
     1.6  fun overwrite_warn (args as (alist, (a, _))) msg =
     1.7 - (if is_none (assoc (alist, a)) then () else warning msg;
     1.8 + (if is_none (AList.lookup (op =) alist a) then () else warning msg;
     1.9    overwrite args);
    1.10  
    1.11 -
    1.12 +fun update_warn eq msg (kv as (key, value)) xs = (
    1.13 +  if (not o AList.defined eq xs) key then () else warning msg;
    1.14 +  AList.update eq kv xs
    1.15 +)
    1.16  
    1.17  (** handle errors  **)
    1.18