summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Wed, 31 Aug 2005 09:01:45 +0200 | |

changeset 17191 | ae9901f856aa |

parent 17190 | 5fc6a0666094 |

child 17192 | 0cfbf76ed313 |

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;