diff -r 464913c6086a -r 9125611c1645 src/Pure/General/name_space.ML
--- 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 *)