--- a/src/Pure/General/name_space.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/General/name_space.ML Fri Mar 04 15:07:34 2005 +0100
@@ -102,7 +102,7 @@
error ("Attempt to declare hidden name " ^ quote name)
else Library.foldl (fn (tb, xname) => change add xname (name, tb)) (tab, accesses name);
-fun extend (NameSpace tab, names) = NameSpace (Library.foldr extend_aux (names, tab));
+fun extend (NameSpace tab, names) = NameSpace (foldr extend_aux tab names);
(* merge *) (*1st preferred over 2nd*)
@@ -126,7 +126,7 @@
Library.foldl (fn (tb, xname) => change del xname (name, tb))
(tab, if fully then accesses name else [base name])));
-fun hide fully (NameSpace tab, names) = NameSpace (Library.foldr (hide_aux fully) (names, tab));
+fun hide fully (NameSpace tab, names) = NameSpace (foldr (hide_aux fully) tab names);
(* intern / extern names *)