1.1 --- a/src/Pure/Isar/local_theory.ML	Thu Mar 19 11:20:22 2009 +0100
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Thu Mar 19 11:44:34 2009 +0100
     1.3 @@ -23,6 +23,7 @@
     1.4    val theory: (theory -> theory) -> local_theory -> local_theory
     1.5    val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
     1.6    val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
     1.7 +  val map_contexts: (Context.generic -> Context.generic) -> local_theory -> local_theory
     1.8    val affirm: local_theory -> local_theory
     1.9    val pretty: local_theory -> Pretty.T list
    1.10    val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
    1.11 @@ -163,6 +164,11 @@
    1.12  
    1.13  fun target f = #2 o target_result (f #> pair ());
    1.14  
    1.15 +fun map_contexts f =
    1.16 +  theory (Context.theory_map f) #>
    1.17 +  target (Context.proof_map f) #>
    1.18 +  Context.proof_map f;
    1.19 +
    1.20  
    1.21  (* basic operations *)
    1.22