src/Pure/General/binding.ML

   val suffix_name: string -> binding -> binding
   val eq_name: binding * binding -> bool
   val empty: binding
   val is_empty: binding -> bool
   val qualify: bool -> string -> binding -> binding
+  val qualified: bool -> string -> binding -> binding
   val qualified_name: string -> binding
   val qualified_name_of: binding -> string
   val prefix_of: binding -> (string * bool) list
   val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
   val prefix: bool -> string -> binding -> binding

 fun qualify _ "" = I
   | qualify mandatory qual =
       map_binding (fn (conceal, prefix, qualifier, name, pos) =>
         (conceal, prefix, (qual, mandatory) :: qualifier, name, pos));
 
+fun qualified mandatory name' = map_binding (fn (conceal, prefix, qualifier, name, pos) =>
+  let val qualifier' = if name = "" then qualifier else qualifier @ [(name, mandatory)]
+  in (conceal, prefix, qualifier', name', pos) end);
+
 fun qualified_name "" = empty
   | qualified_name s =
       let val (qualifier, name) = split_last (Long_Name.explode s)
       in make_binding (false, [], map (rpair false) qualifier, name, Position.none) end;