src/Pure/Isar/proof_context.ML

   val get_thm_closure: Proof.context -> thmref -> thm
   val get_thms: Proof.context -> thmref -> thm list
   val get_thms_closure: Proof.context -> thmref -> thm list
   val valid_thms: Proof.context -> string * thm list -> bool
   val lthms_containing: Proof.context -> FactIndex.spec -> (string * thm list) list
+  val add_path: string -> Proof.context -> Proof.context
   val no_base_names: 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

     else (NameSpace.hidden (if name = "" then "unnamed" else name), ths));
 
 
 (* name space operations *)
 
+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 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);