diff -r 2e37cdae7b9c -r aaddb2b526d6 src/Pure/General/name_space.ML
--- 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 *)