src/Pure/General/name_space.ML
changeset 15574 b1d1b5bfc464
parent 15570 8d8c70b41bab
child 15624 484178635bd8
--- 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 *)