# HG changeset patch
# User wenzelm
# Date 1256747794 -3600
# Node ID 223ef9bc399ad1b1fe05019e296ef6d741143076
# Parent  e3eaeba6ae28ec3b0be02f1ce26dce893fc42ba4
let naming transform binding beforehand -- covering only the "conceal" flag for now;
export LocalTheory.standard_morphism;

diff -r e3eaeba6ae28 -r 223ef9bc399a src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Wed Oct 28 16:28:12 2009 +0100
+++ b/src/Pure/General/name_space.ML	Wed Oct 28 17:36:34 2009 +0100
@@ -40,6 +40,7 @@
   val root_path: naming -> naming
   val parent_path: naming -> naming
   val mandatory_path: string -> naming -> naming
+  val transform_binding: naming -> binding -> binding
   val full_name: naming -> binding -> string
   val external_names: naming -> string -> string list
   val declare: bool -> naming -> binding -> T -> string * T
@@ -254,14 +255,17 @@
 
 (* full name *)
 
+fun transform_binding (Naming {conceal = true, ...}) = Binding.conceal
+  | transform_binding _ = I;
+
 fun err_bad binding = error ("Bad name binding " ^ quote (Binding.str_of binding));
 
-fun name_spec (Naming {conceal = conceal1, path, ...}) binding =
+fun name_spec (naming as Naming {path, ...}) raw_binding =
   let
-    val (conceal2, prefix, name) = Binding.dest binding;
+    val binding = transform_binding naming raw_binding;
+    val (concealed, prefix, name) = Binding.dest binding;
     val _ = Long_Name.is_qualified name andalso err_bad binding;
 
-    val concealed = conceal1 orelse conceal2;
     val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix);
     val spec2 = if name = "" then [] else [(name, true)];
     val spec = spec1 @ spec2;
diff -r e3eaeba6ae28 -r 223ef9bc399a src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Wed Oct 28 16:28:12 2009 +0100
+++ b/src/Pure/Isar/local_theory.ML	Wed Oct 28 17:36:34 2009 +0100
@@ -25,6 +25,8 @@
   val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
   val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
   val map_contexts: (Context.generic -> Context.generic) -> local_theory -> local_theory
+  val standard_morphism: local_theory -> Proof.context -> morphism
+  val target_morphism: local_theory -> morphism
   val pretty: local_theory -> Pretty.T list
   val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
@@ -37,7 +39,6 @@
   val term_syntax: declaration -> local_theory -> local_theory
   val declaration: declaration -> local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
-  val target_morphism: local_theory -> morphism
   val init: string -> operations -> Proof.context -> local_theory
   val restore: local_theory -> local_theory
   val reinit: local_theory -> local_theory
@@ -166,6 +167,15 @@
   Context.proof_map f;
 
 
+(* morphisms *)
+
+fun standard_morphism lthy ctxt =
+  ProofContext.norm_export_morphism lthy ctxt $>
+  Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
+
+fun target_morphism lthy = standard_morphism lthy (target_of lthy);
+
+
 (* basic operations *)
 
 fun operation f lthy = f (#operations (get_lthy lthy)) lthy;
@@ -182,9 +192,6 @@
 
 fun note kind (a, ths) = notes kind [(a, [(ths, [])])] #>> the_single;
 
-fun target_morphism lthy =
-  ProofContext.norm_export_morphism lthy (target_of lthy);
-
 fun notation add mode raw_args lthy =
   let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
   in term_syntax (ProofContext.target_notation add mode args) lthy end;
@@ -218,14 +225,14 @@
 fun exit_result f (x, lthy) =
   let
     val ctxt = exit lthy;
-    val phi = ProofContext.norm_export_morphism lthy ctxt;
+    val phi = standard_morphism lthy ctxt;
   in (f phi x, ctxt) end;
 
 fun exit_result_global f (x, lthy) =
   let
     val thy = exit_global lthy;
     val thy_ctxt = ProofContext.init thy;
-    val phi = ProofContext.norm_export_morphism lthy thy_ctxt;
+    val phi = standard_morphism lthy thy_ctxt;
   in (f phi x, thy) end;
 
 end;