better map_entry

--- a/src/Pure/General/alist.ML	Tue Aug 30 21:32:10 2005 +0200
+++ b/src/Pure/General/alist.ML	Wed Aug 31 09:01:45 2005 +0200
@@ -44,11 +44,6 @@
 fun default eq (key, value) xs =
   if defined eq xs key then xs else (key, value)::xs;
 
-fun map_entry eq _ _ [] = []
-  | map_entry eq key' f ((x as (key, value))::xs) =
-      if eq (key', key) then ((key, f value)::xs)
-      else x :: map_entry eq key' f xs;
-
 fun delete eq key xs =
   let
     fun del ((x as (key', _))::xs) =
@@ -56,4 +51,11 @@
       else x :: del xs;
   in if defined eq xs key then del xs else xs end;
 
+fun map_entry eq key' f xs =
+  let
+    fun mapp ((x as (key, value))::xs) =
+      if eq (key', key) then (key, f value)::xs
+      else x :: mapp xs
+  in if defined eq xs key' then mapp xs else xs end;
+
 end;