# HG changeset patch # User berghofe # Date 1064240386 -7200 # Node ID 8ea2645b813231fdba312c2ee188667f490e8d03 # Parent 3d7c6fc7c66e3fed35313c3a1641b3c08db43255 Modified merge_aux to prevent newer names from getting overwritten by older names. diff -r 3d7c6fc7c66e -r 8ea2645b8132 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Mon Sep 22 16:16:03 2003 +0200 +++ b/src/Pure/General/name_space.ML Mon Sep 22 16:19:46 2003 +0200 @@ -106,8 +106,9 @@ (* merge *) (*1st preferred over 2nd*) -fun merge_aux (tab, (xname, (names, names'))) = - foldr (change add xname) (names, foldr (change' add xname) (names', tab)); +fun merge_aux (tab, (xname, (names1, names1'))) = + map_space (fn (names2, names2') => + (merge_lists' names2 names1, merge_lists' names2' names1')) xname tab; fun merge (NameSpace tab1, NameSpace tab2) = NameSpace (Symtab.foldl merge_aux (tab2, tab1));