--- a/src/Pure/sign.ML Sat Feb 11 17:17:47 2006 +0100
+++ b/src/Pure/sign.ML Sat Feb 11 17:17:48 2006 +0100
@@ -64,9 +64,9 @@
val root_path: theory -> theory
val absolute_path: theory -> theory
val local_path: theory -> theory
+ val no_base_names: theory -> theory
val qualified_names: theory -> theory
- val no_base_names: theory -> theory
- val custom_accesses: (string list -> string list list) -> theory -> theory
+ val qualified_force_prefix: string -> theory -> theory
val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
theory -> theory
val restore_naming: theory -> theory -> theory
@@ -884,16 +884,16 @@
(* modify naming *)
-val add_path = map_naming o NameSpace.add_path;
-val qualified_names = map_naming NameSpace.qualified_names;
-val no_base_names = map_naming NameSpace.no_base_names;
-val custom_accesses = map_naming o NameSpace.custom_accesses;
-val set_policy = map_naming o NameSpace.set_policy;
-val restore_naming = map_naming o K o naming_of;
+val add_path = map_naming o NameSpace.add_path;
+val no_base_names = map_naming NameSpace.no_base_names;
+val qualified_names = map_naming NameSpace.qualified_names;
+val qualified_force_prefix = map_naming o NameSpace.qualified_force_prefix;
+val set_policy = map_naming o NameSpace.set_policy;
+val restore_naming = map_naming o K o naming_of;
-val parent_path = add_path "..";
-val root_path = add_path "/";
-val absolute_path = add_path "//";
+val parent_path = add_path "..";
+val root_path = add_path "/";
+val absolute_path = add_path "//";
fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);