changeset 18011 | 685d95c793ff |
parent 17756 | d4a35f82fbb4 |
child 18939 | 18e2a2676d80 |
--- a/src/Pure/General/name_space.ML Fri Oct 28 13:52:57 2005 +0200 +++ b/src/Pure/General/name_space.ML Fri Oct 28 16:35:40 2005 +0200 @@ -89,7 +89,7 @@ fun map_base _ "" = "" | map_base f name = let val names = unpack name - in pack (map_nth_elem (length names - 1) f names) end; + in pack (nth_map (length names - 1) f names) end; fun suffixes_prefixes xs = let