src/Pure/Isar/local_theory.ML
changeset 33281 223ef9bc399a
parent 33276 f2bc8bc6e73d
child 33383 12d79ece3f7e
     1.1 --- a/src/Pure/Isar/local_theory.ML	Wed Oct 28 16:28:12 2009 +0100
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Wed Oct 28 17:36:34 2009 +0100
     1.3 @@ -25,6 +25,8 @@
     1.4    val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
     1.5    val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
     1.6    val map_contexts: (Context.generic -> Context.generic) -> local_theory -> local_theory
     1.7 +  val standard_morphism: local_theory -> Proof.context -> morphism
     1.8 +  val target_morphism: local_theory -> morphism
     1.9    val pretty: local_theory -> Pretty.T list
    1.10    val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
    1.11      (term * term) * local_theory
    1.12 @@ -37,7 +39,6 @@
    1.13    val term_syntax: declaration -> local_theory -> local_theory
    1.14    val declaration: declaration -> local_theory -> local_theory
    1.15    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    1.16 -  val target_morphism: local_theory -> morphism
    1.17    val init: string -> operations -> Proof.context -> local_theory
    1.18    val restore: local_theory -> local_theory
    1.19    val reinit: local_theory -> local_theory
    1.20 @@ -166,6 +167,15 @@
    1.21    Context.proof_map f;
    1.22  
    1.23  
    1.24 +(* morphisms *)
    1.25 +
    1.26 +fun standard_morphism lthy ctxt =
    1.27 +  ProofContext.norm_export_morphism lthy ctxt $>
    1.28 +  Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
    1.29 +
    1.30 +fun target_morphism lthy = standard_morphism lthy (target_of lthy);
    1.31 +
    1.32 +
    1.33  (* basic operations *)
    1.34  
    1.35  fun operation f lthy = f (#operations (get_lthy lthy)) lthy;
    1.36 @@ -182,9 +192,6 @@
    1.37  
    1.38  fun note kind (a, ths) = notes kind [(a, [(ths, [])])] #>> the_single;
    1.39  
    1.40 -fun target_morphism lthy =
    1.41 -  ProofContext.norm_export_morphism lthy (target_of lthy);
    1.42 -
    1.43  fun notation add mode raw_args lthy =
    1.44    let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
    1.45    in term_syntax (ProofContext.target_notation add mode args) lthy end;
    1.46 @@ -218,14 +225,14 @@
    1.47  fun exit_result f (x, lthy) =
    1.48    let
    1.49      val ctxt = exit lthy;
    1.50 -    val phi = ProofContext.norm_export_morphism lthy ctxt;
    1.51 +    val phi = standard_morphism lthy ctxt;
    1.52    in (f phi x, ctxt) end;
    1.53  
    1.54  fun exit_result_global f (x, lthy) =
    1.55    let
    1.56      val thy = exit_global lthy;
    1.57      val thy_ctxt = ProofContext.init thy;
    1.58 -    val phi = ProofContext.norm_export_morphism lthy thy_ctxt;
    1.59 +    val phi = standard_morphism lthy thy_ctxt;
    1.60    in (f phi x, thy) end;
    1.61  
    1.62  end;