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