# HG changeset patch
# User wenzelm
# Date 1140035706 -3600
# Node ID 4f408867f9d42fe591524ffbf265cbd7bcf8687d
# Parent  af7cc6063285d702e017ecef1be5df9e6e6f06d4
removed qualified_force_prefix;
added sticky_prefix;

diff -r af7cc6063285 -r 4f408867f9d4 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Wed Feb 15 21:35:04 2006 +0100
+++ b/src/Pure/General/name_space.ML	Wed Feb 15 21:35:06 2006 +0100
@@ -48,7 +48,7 @@
   val add_path: string -> naming -> naming
   val no_base_names: naming -> naming
   val qualified_names: naming -> naming
-  val qualified_force_prefix: string -> naming -> naming
+  val sticky_prefix: string -> naming -> naming
   val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
     naming -> naming
   type 'a table (*= T * 'a Symtab.table*)
@@ -256,9 +256,9 @@
 
 fun qualified_names (Naming (path, (_, accs))) = Naming (path, (qualified, accs));
 
-fun qualified_force_prefix prfx (Naming (path, _)) =
-  Naming (path,
-    (qualified, suffixes_prefixes_split (length (unpack path)) (length (unpack prfx))));
+fun sticky_prefix prfx (Naming (path, (qualify, _))) =
+  Naming (append path prfx,
+    (qualify, suffixes_prefixes_split (length (unpack path)) (length (unpack prfx))));
 
 fun set_policy policy (Naming (path, _)) = Naming (path, policy);