src/Pure/name_space.ML
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;