src/Pure/General/name_space.ML
changeset 19055 4f408867f9d4
parent 19030 78d43fe9ac65
child 19305 5c16895d548b
--- 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);