# HG changeset patch
# User haftmann
# Date 1125471705 -7200
# Node ID ae9901f856aabcf2aff1688bb7f4fd11ee5f262f
# Parent  5fc6a0666094aabc35c8890f84d401352e7cae75
better map_entry

diff -r 5fc6a0666094 -r ae9901f856aa src/Pure/General/alist.ML
--- 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;