tuned;
authorwenzelm
Mon Sep 04 21:18:33 2000 +0200 (2000-09-04)
changeset 9830e4ad74159b43
parent 9829 bf49c3796599
child 9831 9b883c416aef
tuned;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Mon Sep 04 21:18:28 2000 +0200
     1.2 +++ b/src/Pure/library.ML	Mon Sep 04 21:18:33 2000 +0200
     1.3 @@ -1209,9 +1209,9 @@
     1.4  
     1.5  (** misc **)
     1.6  
     1.7 -fun overwrite_warn (args as (alist,(a,_))) text =
     1.8 -  (if is_none(assoc(alist,a)) then () else warning text;
     1.9 -   overwrite args);
    1.10 +fun overwrite_warn (args as (alist, (a, _))) msg =
    1.11 + (if is_none (assoc (alist, a)) then () else warning msg;
    1.12 +  overwrite args);
    1.13  
    1.14  (*use the keyfun to make a list of (x, key) pairs*)
    1.15  fun make_keylist (keyfun: 'a->'b) : 'a list -> ('a * 'b) list =