# HG changeset patch
# User wenzelm
# Date 1144529482 -7200
# Node ID 6af9ee48b563a9c18530816d9050546a2c6e6678
# Parent  a2040baa9444038ec7190b3cdb91ae711becd768
tuned;

diff -r a2040baa9444 -r 6af9ee48b563 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sat Apr 08 22:51:20 2006 +0200
+++ b/src/Pure/General/name_space.ML	Sat Apr 08 22:51:22 2006 +0200
@@ -275,7 +275,7 @@
   in (fold (declare naming o #1) entries space, Symtab.extend (tab, entries)) end;
 
 fun merge_tables eq ((space1, tab1), (space2, tab2)) =
-  (merge (space1, space2), (Symtab.merge eq (tab1, tab2)));
+  (merge (space1, space2), Symtab.merge eq (tab1, tab2));
 
 fun ext_table (space, tab) =
   Symtab.fold (fn (name, x) => cons ((name, extern space name), x)) tab []