src/Pure/General/name_space.ML
changeset 30469 de9e8f1d927c
parent 30465 038839f111a1
child 30522 e26b80647189
     1.1 --- a/src/Pure/General/name_space.ML	Thu Mar 12 12:04:27 2009 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Thu Mar 12 13:18:42 2009 +0100
     1.3 @@ -36,7 +36,7 @@
     1.4    val root_path: naming -> naming
     1.5    val parent_path: naming -> naming
     1.6    val no_base_names: naming -> naming
     1.7 -  val sticky_prefix: string -> naming -> naming
     1.8 +  val mandatory_path: string -> naming -> naming
     1.9    type 'a table = T * 'a Symtab.table
    1.10    val define: naming -> binding * 'a -> 'a table -> string * 'a table (*exception Symtab.DUP*)
    1.11    val empty_table: 'a table
    1.12 @@ -194,7 +194,7 @@
    1.13  val parent_path = map_naming (fn (path, no_base_names) =>
    1.14    (perhaps (try (#1 o split_last)) path, no_base_names));
    1.15  
    1.16 -fun sticky_prefix elems = map_naming (fn (path, no_base_names) =>
    1.17 +fun mandatory_path elems = map_naming (fn (path, no_base_names) =>
    1.18    (path @ [(elems, true)], no_base_names));
    1.19  
    1.20  val no_base_names = map_naming (fn (path, _) => (path, true));