src/Pure/General/binding.ML

--- a/src/Pure/General/binding.ML	Thu Feb 18 20:44:22 2010 +0100
+++ b/src/Pure/General/binding.ML	Thu Feb 18 20:46:46 2010 +0100
@@ -22,6 +22,7 @@
   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
@@ -87,6 +88,10 @@
       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)