src/Pure/General/name_space.ML
changeset 19367 6af9ee48b563
parent 19305 5c16895d548b
child 20530 448594cbd82b
     1.1 --- a/src/Pure/General/name_space.ML	Sat Apr 08 22:51:20 2006 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Sat Apr 08 22:51:22 2006 +0200
     1.3 @@ -275,7 +275,7 @@
     1.4    in (fold (declare naming o #1) entries space, Symtab.extend (tab, entries)) end;
     1.5  
     1.6  fun merge_tables eq ((space1, tab1), (space2, tab2)) =
     1.7 -  (merge (space1, space2), (Symtab.merge eq (tab1, tab2)));
     1.8 +  (merge (space1, space2), Symtab.merge eq (tab1, tab2));
     1.9  
    1.10  fun ext_table (space, tab) =
    1.11    Symtab.fold (fn (name, x) => cons ((name, extern space name), x)) tab []