changeset 3876 | e6f918979f2d |
parent 3833 | 370e845c391f |
child 3972 | 87941982f475 |
--- a/src/Pure/name_space.ML Wed Oct 15 15:14:56 1997 +0200 +++ b/src/Pure/name_space.ML Wed Oct 15 15:15:22 1997 +0200 @@ -25,7 +25,7 @@ val prune: T -> string -> string end; -structure NameSpace(*: NAME_SPACE FIXME *) = +structure NameSpace: NAME_SPACE = struct @@ -61,7 +61,7 @@ fun make entries = let - fun accesses [] = [] (* FIXME !? *) + fun accesses [] = [] | accesses entry = let val p = pack entry;