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