src/Pure/sign.ML

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