src/Pure/sign.ML
changeset 35200 aaddb2b526d6
parent 35129 ed24ba6f69aa
child 35255 2cb27605301f
     1.1 --- a/src/Pure/sign.ML	Thu Feb 18 20:44:22 2010 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Feb 18 20:46:46 2010 +0100
     1.3 @@ -127,6 +127,7 @@
     1.4    val root_path: theory -> theory
     1.5    val parent_path: theory -> theory
     1.6    val mandatory_path: string -> theory -> theory
     1.7 +  val qualified_path: bool -> binding -> theory -> theory
     1.8    val local_path: theory -> theory
     1.9    val restore_naming: theory -> theory -> theory
    1.10    val hide_class: bool -> string -> theory -> theory
    1.11 @@ -614,6 +615,7 @@
    1.12  val root_path = map_naming Name_Space.root_path;
    1.13  val parent_path = map_naming Name_Space.parent_path;
    1.14  val mandatory_path = map_naming o Name_Space.mandatory_path;
    1.15 +val qualified_path = map_naming oo Name_Space.qualified_path;
    1.16  
    1.17  fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
    1.18