src/Pure/Isar/proof_context.ML

   val get_fact: Proof.context -> Facts.ref -> thm list
   val get_fact_single: Proof.context -> Facts.ref -> thm
   val get_thms: Proof.context -> xstring -> thm list
   val get_thm: Proof.context -> xstring -> thm
   val add_path: string -> Proof.context -> Proof.context
-  val no_base_names: Proof.context -> Proof.context
+  val sticky_prefix: string -> Proof.context -> Proof.context
   val qualified_names: Proof.context -> Proof.context
-  val sticky_prefix: string -> Proof.context -> Proof.context
   val restore_naming: Proof.context -> Proof.context -> Proof.context
   val reset_naming: Proof.context -> Proof.context
   val note_thmss: string -> (Thm.binding * (Facts.ref * attribute list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
   val note_thmss_i: string -> (Thm.binding * (thm list * attribute list) list) list ->

 
 
 (* name space operations *)
 
 val add_path        = map_naming o NameSpace.add_path;
-val no_base_names   = map_naming NameSpace.no_base_names;
+val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
 val qualified_names = map_naming NameSpace.qualified_names;
-val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
 val restore_naming  = map_naming o K o naming_of;
 val reset_naming    = map_naming (K local_naming);
 
 
 (* facts *)