# HG changeset patch
# User wenzelm
# Date 1170023357 -3600
# Node ID efc0cdc013077bc5b95a1f1b61744aa0aee18165
# Parent  0544af1a5117b0f9ab766a9ec3cff55cd3d5c58c
added interface for target_naming;

diff -r 0544af1a5117 -r efc0cdc01307 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 *)
 
diff -r 0544af1a5117 -r efc0cdc01307 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Sun Jan 28 23:29:16 2007 +0100
+++ b/src/Pure/Isar/theory_target.ML	Sun Jan 28 23:29:17 2007 +0100
@@ -295,11 +295,10 @@
   ProofContext.export_morphism lthy (LocalTheory.target_of lthy) $>
   Morphism.thm_morphism Goal.norm_result;
 
-fun target_name loc lthy =
+fun target_naming loc lthy =
   (if loc = "" then Sign.naming_of (ProofContext.theory_of lthy)
    else ProofContext.naming_of (LocalTheory.target_of lthy))
-  |> NameSpace.qualified_names
-  |> NameSpace.full;
+  |> NameSpace.qualified_names;
 
 
 (* init and exit *)
@@ -318,7 +317,7 @@
       term_syntax = term_syntax loc,
       declaration = declaration loc,
       target_morphism = target_morphism loc,
-      target_name = target_name loc,
+      target_naming = target_naming loc,
       reinit = fn _ =>
         begin is_class loc o (if is_loc then Locale.init loc else ProofContext.init),
       exit = LocalTheory.target_of}