src/Pure/name.ML

--- a/src/Pure/name.ML	Thu Nov 13 01:31:20 2008 +0100
+++ b/src/Pure/name.ML	Thu Nov 13 14:19:07 2008 +0100
@@ -38,6 +38,7 @@
   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 =
@@ -171,4 +172,8 @@
 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;