src/Pure/General/name_space.ML

   val reset_group: naming -> naming
   val add_path: string -> naming -> naming
   val root_path: naming -> naming
   val parent_path: naming -> naming
   val mandatory_path: string -> naming -> naming
+  val qualified_path: bool -> binding -> naming -> naming
   val transform_binding: naming -> binding -> binding
   val full_name: naming -> binding -> string
   val external_names: naming -> string -> string list
   val declare: bool -> naming -> binding -> T -> string * T
   type 'a table = T * 'a Symtab.table

 fun add_path elems = map_path (fn path => path @ [(elems, false)]);
 val root_path = map_path (fn _ => []);
 val parent_path = map_path (perhaps (try (#1 o split_last)));
 fun mandatory_path elems = map_path (fn path => path @ [(elems, true)]);
 
+fun qualified_path mandatory binding = map_path (fn path =>
+  path @ #2 (Binding.dest (Binding.qualified mandatory "" binding)));
+
 
 (* full name *)
 
 fun transform_binding (Naming {conceal = true, ...}) = Binding.conceal
   | transform_binding _ = I;