src/Pure/sign.ML
changeset 19013 19ad0c59fb1f
parent 18994 ce724d5bada2
child 19054 af7cc6063285
     1.1 --- a/src/Pure/sign.ML	Sat Feb 11 17:17:47 2006 +0100
     1.2 +++ b/src/Pure/sign.ML	Sat Feb 11 17:17:48 2006 +0100
     1.3 @@ -64,9 +64,9 @@
     1.4    val root_path: theory -> theory
     1.5    val absolute_path: theory -> theory
     1.6    val local_path: theory -> theory
     1.7 +  val no_base_names: theory -> theory
     1.8    val qualified_names: theory -> theory
     1.9 -  val no_base_names: theory -> theory
    1.10 -  val custom_accesses: (string list -> string list list) -> theory -> theory
    1.11 +  val qualified_force_prefix: string -> theory -> theory
    1.12    val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
    1.13      theory -> theory
    1.14    val restore_naming: theory -> theory -> theory
    1.15 @@ -884,16 +884,16 @@
    1.16  
    1.17  (* modify naming *)
    1.18  
    1.19 -val add_path        = map_naming o NameSpace.add_path;
    1.20 -val qualified_names = map_naming NameSpace.qualified_names;
    1.21 -val no_base_names   = map_naming NameSpace.no_base_names;
    1.22 -val custom_accesses = map_naming o NameSpace.custom_accesses;
    1.23 -val set_policy      = map_naming o NameSpace.set_policy;
    1.24 -val restore_naming  = map_naming o K o naming_of;
    1.25 +val add_path               = map_naming o NameSpace.add_path;
    1.26 +val no_base_names          = map_naming NameSpace.no_base_names;
    1.27 +val qualified_names        = map_naming NameSpace.qualified_names;
    1.28 +val qualified_force_prefix = map_naming o NameSpace.qualified_force_prefix;
    1.29 +val set_policy             = map_naming o NameSpace.set_policy;
    1.30 +val restore_naming         = map_naming o K o naming_of;
    1.31  
    1.32 -val parent_path     = add_path "..";
    1.33 -val root_path       = add_path "/";
    1.34 -val absolute_path   = add_path "//";
    1.35 +val parent_path   = add_path "..";
    1.36 +val root_path     = add_path "/";
    1.37 +val absolute_path = add_path "//";
    1.38  
    1.39  fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
    1.40