1.1 --- a/src/Pure/General/binding.ML	Thu Feb 18 20:44:22 2010 +0100
     1.2 +++ b/src/Pure/General/binding.ML	Thu Feb 18 20:46:46 2010 +0100
     1.3 @@ -22,6 +22,7 @@
     1.4    val empty: binding
     1.5    val is_empty: binding -> bool
     1.6    val qualify: bool -> string -> binding -> binding
     1.7 +  val qualified: bool -> string -> binding -> binding
     1.8    val qualified_name: string -> binding
     1.9    val qualified_name_of: binding -> string
    1.10    val prefix_of: binding -> (string * bool) list
    1.11 @@ -87,6 +88,10 @@
    1.12        map_binding (fn (conceal, prefix, qualifier, name, pos) =>
    1.13          (conceal, prefix, (qual, mandatory) :: qualifier, name, pos));
    1.14  
    1.15 +fun qualified mandatory name' = map_binding (fn (conceal, prefix, qualifier, name, pos) =>
    1.16 +  let val qualifier' = if name = "" then qualifier else qualifier @ [(name, mandatory)]
    1.17 +  in (conceal, prefix, qualifier', name', pos) end);
    1.18 +
    1.19  fun qualified_name "" = empty
    1.20    | qualified_name s =
    1.21        let val (qualifier, name) = split_last (Long_Name.explode s)

     2.1 --- a/src/Pure/General/name_space.ML	Thu Feb 18 20:44:22 2010 +0100
     2.2 +++ b/src/Pure/General/name_space.ML	Thu Feb 18 20:46:46 2010 +0100
     2.3 @@ -43,6 +43,7 @@
     2.4    val root_path: naming -> naming
     2.5    val parent_path: naming -> naming
     2.6    val mandatory_path: string -> naming -> naming
     2.7 +  val qualified_path: bool -> binding -> naming -> naming
     2.8    val transform_binding: naming -> binding -> binding
     2.9    val full_name: naming -> binding -> string
    2.10    val external_names: naming -> string -> string list
    2.11 @@ -261,6 +262,9 @@
    2.12  val parent_path = map_path (perhaps (try (#1 o split_last)));
    2.13  fun mandatory_path elems = map_path (fn path => path @ [(elems, true)]);
    2.14  
    2.15 +fun qualified_path mandatory binding = map_path (fn path =>
    2.16 +  path @ #2 (Binding.dest (Binding.qualified mandatory "" binding)));
    2.17 +
    2.18  
    2.19  (* full name *)
    2.20  

     3.1 --- a/src/Pure/sign.ML	Thu Feb 18 20:44:22 2010 +0100
     3.2 +++ b/src/Pure/sign.ML	Thu Feb 18 20:46:46 2010 +0100
     3.3 @@ -127,6 +127,7 @@
     3.4    val root_path: theory -> theory
     3.5    val parent_path: theory -> theory
     3.6    val mandatory_path: string -> theory -> theory
     3.7 +  val qualified_path: bool -> binding -> theory -> theory
     3.8    val local_path: theory -> theory
     3.9    val restore_naming: theory -> theory -> theory
    3.10    val hide_class: bool -> string -> theory -> theory
    3.11 @@ -614,6 +615,7 @@
    3.12  val root_path = map_naming Name_Space.root_path;
    3.13  val parent_path = map_naming Name_Space.parent_path;
    3.14  val mandatory_path = map_naming o Name_Space.mandatory_path;
    3.15 +val qualified_path = map_naming oo Name_Space.qualified_path;
    3.16  
    3.17  fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
    3.18