| changeset 5682 | 9125611c1645 |
| parent 5175 | 2dbef0104bcf |
| child 6118 | caa439435666 |
--- a/src/Pure/General/name_space.ML Tue Oct 20 16:19:53 1998 +0200 +++ b/src/Pure/General/name_space.ML Tue Oct 20 16:20:19 1998 +0200 @@ -82,7 +82,7 @@ NameSpace (foldl add (tab, flat (map (fn name => map (rpair name) (accesses name)) names))); fun merge (NameSpace tab1, NameSpace tab2) = (*2nd overrides 1st*) - NameSpace (foldl add (tab1, Symtab.dest tab2)); + NameSpace (Symtab.foldl add (tab1, tab2)); (* intern / extern names *)