# HG changeset patch
# User wenzelm
# Date 908893219 -7200
# Node ID 9125611c16457b21758441390d62ea58d5f6f82b
# Parent  464913c6086ae770dc67d1045ff8277b0fb38247
Symtab.foldl;

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 *)