src/Pure/name.ML

   val name_of: binding -> string
   val pos_of: binding -> Position.T
   val add_prefix: bool -> string -> binding -> binding
   val map_name: (string -> string) -> binding -> binding
   val qualified: string -> binding -> binding
+  val output: binding -> string
 end;
 
 structure Name: NAME =
 struct
 

   (cons (prfx, sticky));
 
 val map_name = map_binding o apfst o apsnd;
 val qualified = map_name o NameSpace.qualified;
 
+fun output (Binding ((prefix, name), _)) =
+  if null prefix orelse name = "" then name
+  else NameSpace.implode (map fst prefix) ^ " / " ^ name;
+
 end;