src/Pure/Isar/local_theory.ML

--- a/src/Pure/Isar/local_theory.ML	Sun Jan 28 23:29:16 2007 +0100
+++ b/src/Pure/Isar/local_theory.ML	Sun Jan 28 23:29:17 2007 +0100
@@ -39,6 +39,7 @@
     local_theory -> (bstring * thm list) * Proof.context
   val notation: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val target_morphism: local_theory -> morphism
+  val target_naming: local_theory -> NameSpace.naming
   val target_name: local_theory -> bstring -> string
   val init: string -> operations -> Proof.context -> local_theory
   val restore: local_theory -> local_theory
@@ -69,7 +70,7 @@
   term_syntax: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory,
   declaration: (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory,
   target_morphism: local_theory -> morphism,
-  target_name: local_theory -> bstring -> string,
+  target_naming: local_theory -> NameSpace.naming,
   reinit: local_theory -> theory -> local_theory,
   exit: local_theory -> Proof.context};
 
@@ -164,7 +165,7 @@
 val term_syntax = operation1 #term_syntax;
 val declaration = operation1 #declaration;
 val target_morphism = operation #target_morphism;
-val target_name = operation #target_name;
+val target_naming = operation #target_naming;
 
 fun def kind arg lthy = lthy |> defs kind [arg] |>> hd;
 fun note kind (a, ths) lthy = lthy |> notes kind [(a, [(ths, [])])] |>> hd;
@@ -173,6 +174,8 @@
   let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
   in term_syntax (ProofContext.target_notation mode args) lthy end;
 
+val target_name = NameSpace.full o target_naming;
+
 
 (* init -- exit *)