# HG changeset patch
# User wenzelm
# Date 1165353293 -3600
# Node ID 2d811ae6752a3c44beac1ac20e37784f4608fade
# Parent  ce813b82c88b43a433f9220c61a0ead9d02b7d53
target_name: allow qualified names;

diff -r ce813b82c88b -r 2d811ae6752a src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Tue Dec 05 22:14:52 2006 +0100
+++ b/src/Pure/Isar/theory_target.ML	Tue Dec 05 22:14:53 2006 +0100
@@ -246,8 +246,7 @@
 fun target_decl _ "" f =
       LocalTheory.theory (Context.theory_map (f Morphism.identity)) #>
       LocalTheory.target (Context.proof_map (f Morphism.identity))
-  | target_decl add loc f =
-      LocalTheory.target (add loc (Context.proof_map o f));
+  | target_decl add loc f = LocalTheory.target (add loc f);
 
 val type_syntax = target_decl Locale.add_type_syntax;
 val term_syntax = target_decl Locale.add_term_syntax;
@@ -257,8 +256,11 @@
   ProofContext.export_morphism lthy (LocalTheory.target_of lthy) $>
   Morphism.thm_morphism Goal.norm_result;
 
-fun target_name "" lthy = Sign.full_name (ProofContext.theory_of lthy)
-  | target_name _ lthy = ProofContext.full_name (LocalTheory.target_of lthy);
+fun target_name 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;
 
 
 (* init and exit *)