more systematic treatment of qualified names derived from binding;

--- 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)

--- a/src/Pure/General/name_space.ML	Thu Feb 18 20:44:22 2010 +0100
+++ b/src/Pure/General/name_space.ML	Thu Feb 18 20:46:46 2010 +0100
@@ -43,6 +43,7 @@
   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
@@ -261,6 +262,9 @@
 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 *)
 

--- a/src/Pure/sign.ML	Thu Feb 18 20:44:22 2010 +0100
+++ b/src/Pure/sign.ML	Thu Feb 18 20:46:46 2010 +0100
@@ -127,6 +127,7 @@
   val root_path: theory -> theory
   val parent_path: theory -> theory
   val mandatory_path: string -> theory -> theory
+  val qualified_path: bool -> binding -> theory -> theory
   val local_path: theory -> theory
   val restore_naming: theory -> theory -> theory
   val hide_class: bool -> string -> theory -> theory
@@ -614,6 +615,7 @@
 val root_path = map_naming Name_Space.root_path;
 val parent_path = map_naming Name_Space.parent_path;
 val mandatory_path = map_naming o Name_Space.mandatory_path;
+val qualified_path = map_naming oo Name_Space.qualified_path;
 
 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);