# HG changeset patch
# User wenzelm
# Date 1139674668 -3600
# Node ID 19ad0c59fb1fc41de5aab88e6e447c6b38efe51b
# Parent  2577ac76cdc62c129bae424172a238d368778d52
removed custom_accesses;
added qualified_force_prefix;

diff -r 2577ac76cdc6 -r 19ad0c59fb1f src/Pure/sign.ML
--- 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);