src/Pure/sign.ML
changeset 30469 de9e8f1d927c
parent 30438 c2d49315b93b
child 30522 e26b80647189
     1.1 --- a/src/Pure/sign.ML	Thu Mar 12 12:04:27 2009 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Mar 12 13:18:42 2009 +0100
     1.3 @@ -124,7 +124,7 @@
     1.4    val add_path: string -> theory -> theory
     1.5    val root_path: theory -> theory
     1.6    val parent_path: theory -> theory
     1.7 -  val sticky_prefix: string -> theory -> theory
     1.8 +  val mandatory_path: string -> theory -> theory
     1.9    val no_base_names: theory -> theory
    1.10    val local_path: theory -> theory
    1.11    val restore_naming: theory -> theory -> theory
    1.12 @@ -619,7 +619,7 @@
    1.13  val add_path        = map_naming o NameSpace.add_path;
    1.14  val root_path       = map_naming NameSpace.root_path;
    1.15  val parent_path     = map_naming NameSpace.parent_path;
    1.16 -val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
    1.17 +val mandatory_path  = map_naming o NameSpace.mandatory_path;
    1.18  val no_base_names   = map_naming NameSpace.no_base_names;
    1.19  
    1.20  fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);