tuned;
authorwenzelm
Thu Aug 14 12:13:24 2014 +0200 (2014-08-14)
changeset 579373bc4725b313e
parent 57936 74ea9ba645c3
child 57938 a9fa81e150c9
tuned;
src/Pure/Isar/attrib.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Thu Aug 14 11:55:09 2014 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Thu Aug 14 12:13:24 2014 +0200
     1.3 @@ -102,10 +102,10 @@
     1.4  
     1.5  val get_attributes = Attributes.get o Context.Proof;
     1.6  
     1.7 -fun transfer_attributes thy ctxt =
     1.8 +fun transfer_attributes ctxt =
     1.9    let
    1.10 -    val attribs' =
    1.11 -      Name_Space.merge_tables (Attributes.get (Context.Theory thy), get_attributes ctxt);
    1.12 +    val attribs0 = Attributes.get (Context.Theory (Proof_Context.theory_of ctxt));
    1.13 +    val attribs' = Name_Space.merge_tables (attribs0, get_attributes ctxt);
    1.14    in Context.proof_map (Attributes.put attribs') ctxt end;
    1.15  
    1.16  fun print_attributes ctxt =
    1.17 @@ -133,16 +133,11 @@
    1.18    in (name, Context.the_theory (Attributes.put attribs' context)) end;
    1.19  
    1.20  fun define binding att comment lthy =
    1.21 -  let
    1.22 -    val standard_morphism =
    1.23 -      Local_Theory.standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
    1.24 -    val att0 = att o Args.transform_values standard_morphism;
    1.25 -  in
    1.26 +  let val att0 = att o Args.transform_values (Local_Theory.background_morphism lthy) in
    1.27      lthy
    1.28      |> Local_Theory.background_theory_result (define_global binding att0 comment)
    1.29      |-> (fn name =>
    1.30 -      Local_Theory.map_contexts
    1.31 -        (fn _ => fn ctxt => transfer_attributes (Proof_Context.theory_of ctxt) ctxt)
    1.32 +      Local_Theory.map_contexts (K transfer_attributes)
    1.33        #> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
    1.34            let
    1.35              val naming = Name_Space.naming_of context;
     2.1 --- a/src/Pure/Isar/local_theory.ML	Thu Aug 14 11:55:09 2014 +0200
     2.2 +++ b/src/Pure/Isar/local_theory.ML	Thu Aug 14 12:13:24 2014 +0200
     2.3 @@ -39,6 +39,7 @@
     2.4    val raw_theory: (theory -> theory) -> local_theory -> local_theory
     2.5    val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
     2.6    val background_theory: (theory -> theory) -> local_theory -> local_theory
     2.7 +  val background_morphism: local_theory -> morphism
     2.8    val target_of: local_theory -> Proof.context
     2.9    val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
    2.10    val target_morphism: local_theory -> morphism
    2.11 @@ -222,6 +223,9 @@
    2.12  
    2.13  fun background_theory f = #2 o background_theory_result (f #> pair ());
    2.14  
    2.15 +fun background_morphism lthy =
    2.16 +  standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
    2.17 +
    2.18  
    2.19  (* target contexts *)
    2.20  
     3.1 --- a/src/Pure/Isar/method.ML	Thu Aug 14 11:55:09 2014 +0200
     3.2 +++ b/src/Pure/Isar/method.ML	Thu Aug 14 12:13:24 2014 +0200
     3.3 @@ -322,10 +322,10 @@
     3.4  
     3.5  val get_methods = Methods.get o Context.Proof;
     3.6  
     3.7 -fun transfer_methods thy ctxt =
     3.8 +fun transfer_methods ctxt =
     3.9    let
    3.10 -    val meths' =
    3.11 -      Name_Space.merge_tables (Methods.get (Context.Theory thy), get_methods ctxt);
    3.12 +    val meths0 = Methods.get (Context.Theory (Proof_Context.theory_of ctxt));
    3.13 +    val meths' = Name_Space.merge_tables (meths0, get_methods ctxt);
    3.14    in Context.proof_map (Methods.put meths') ctxt end;
    3.15  
    3.16  fun print_methods ctxt =
    3.17 @@ -351,16 +351,11 @@
    3.18    in (name, Context.the_theory (Methods.put meths' context)) end;
    3.19  
    3.20  fun define binding meth comment lthy =
    3.21 -  let
    3.22 -    val standard_morphism =
    3.23 -      Local_Theory.standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
    3.24 -    val meth0 = meth o Args.transform_values standard_morphism;
    3.25 -  in
    3.26 +  let val meth0 = meth o Args.transform_values (Local_Theory.background_morphism lthy) in
    3.27      lthy
    3.28      |> Local_Theory.background_theory_result (define_global binding meth0 comment)
    3.29      |-> (fn name =>
    3.30 -      Local_Theory.map_contexts
    3.31 -        (fn _ => fn ctxt => transfer_methods (Proof_Context.theory_of ctxt) ctxt)
    3.32 +      Local_Theory.map_contexts (K transfer_methods)
    3.33        #> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
    3.34            let
    3.35              val naming = Name_Space.naming_of context;