# HG changeset patch
# User wenzelm
# Date 1237459474 -3600
# Node ID 9863745880dbe345a8075016fac92e847b5a0936
# Parent  79cc595655c0270466d519dec8ea9b2415493d90
added map_contexts (cf. Proof.map_contexts);

diff -r 79cc595655c0 -r 9863745880db src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Thu Mar 19 11:20:22 2009 +0100
+++ b/src/Pure/Isar/local_theory.ML	Thu Mar 19 11:44:34 2009 +0100
@@ -23,6 +23,7 @@
   val theory: (theory -> theory) -> local_theory -> local_theory
   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 affirm: local_theory -> local_theory
   val pretty: local_theory -> Pretty.T list
   val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
@@ -163,6 +164,11 @@
 
 fun target f = #2 o target_result (f #> pair ());
 
+fun map_contexts f =
+  theory (Context.theory_map f) #>
+  target (Context.proof_map f) #>
+  Context.proof_map f;
+
 
 (* basic operations *)