src/Pure/sign.ML
changeset 19054 af7cc6063285
parent 19013 19ad0c59fb1f
child 19099 100bf66d7e85
     1.1 --- a/src/Pure/sign.ML	Wed Feb 15 21:35:04 2006 +0100
     1.2 +++ b/src/Pure/sign.ML	Wed Feb 15 21:35:04 2006 +0100
     1.3 @@ -66,7 +66,7 @@
     1.4    val local_path: theory -> theory
     1.5    val no_base_names: theory -> theory
     1.6    val qualified_names: theory -> theory
     1.7 -  val qualified_force_prefix: string -> theory -> theory
     1.8 +  val sticky_prefix: string -> theory -> theory
     1.9    val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
    1.10      theory -> theory
    1.11    val restore_naming: theory -> theory -> theory
    1.12 @@ -884,12 +884,12 @@
    1.13  
    1.14  (* modify naming *)
    1.15  
    1.16 -val add_path               = map_naming o NameSpace.add_path;
    1.17 -val no_base_names          = map_naming NameSpace.no_base_names;
    1.18 -val qualified_names        = map_naming NameSpace.qualified_names;
    1.19 -val qualified_force_prefix = map_naming o NameSpace.qualified_force_prefix;
    1.20 -val set_policy             = map_naming o NameSpace.set_policy;
    1.21 -val restore_naming         = map_naming o K o naming_of;
    1.22 +val add_path        = map_naming o NameSpace.add_path;
    1.23 +val no_base_names   = map_naming NameSpace.no_base_names;
    1.24 +val qualified_names = map_naming NameSpace.qualified_names;
    1.25 +val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
    1.26 +val set_policy      = map_naming o NameSpace.set_policy;
    1.27 +val restore_naming  = map_naming o K o naming_of;
    1.28  
    1.29  val parent_path   = add_path "..";
    1.30  val root_path     = add_path "/";