src/Pure/name.ML

--- a/src/Pure/name.ML	Thu Nov 20 14:55:28 2008 +0100
+++ b/src/Pure/name.ML	Thu Nov 20 19:06:02 2008 +0100
@@ -36,7 +36,6 @@
   val map_name: (string -> string) -> binding -> binding (*FIMXE legacy*)
   val qualified: string -> binding -> binding (*FIMXE legacy*)
   val display: binding -> string
-  val namify: NameSpace.naming -> binding -> NameSpace.naming * string (*FIMXE legacy*)
 end;
 
 structure Name: NAME =
@@ -167,14 +166,6 @@
     val pos = pos_of b;
   in f prefix (binding_pos (name, pos)) end;
 
-fun namify naming b =
-  let
-    val (prefix, name) = dest_binding b
-    fun mk_prefix (prfx, true) = sticky_prefix prfx
-      | mk_prefix (prfx, false) = add_path prfx;
-    val naming' = fold mk_prefix prefix naming;
-  in (naming', full naming' name) end;
-
 fun display b =
   let
     val (prefix, name) = dest_binding b