# HG changeset patch
# User haftmann
# Date 1172216365 -3600
# Node ID f15118a79c0eb57f8fe0942c39c47a7a3aed2e9c
# Parent  587845efb4cfd8b754873054c6674a76f03fb736
add_path for naming in proof contexts

diff -r 587845efb4cf -r f15118a79c0e src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Feb 23 08:39:24 2007 +0100
+++ b/src/Pure/Isar/proof_context.ML	Fri Feb 23 08:39:25 2007 +0100
@@ -104,6 +104,7 @@
   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
@@ -763,6 +764,7 @@
 
 (* 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;