# HG changeset patch
# User wenzelm
# Date 1206814448 -3600
# Node ID b65a5272b360c26c955b1c7002c0857156b7d0cc
# Parent  b90d1fc201de346e525230ce97db1de5dea36e31
added map_theory_result, map_proof_result;

diff -r b90d1fc201de -r b65a5272b360 src/Pure/context.ML
--- a/src/Pure/context.ML	Sat Mar 29 19:14:07 2008 +0100
+++ b/src/Pure/context.ML	Sat Mar 29 19:14:08 2008 +0100
@@ -57,6 +57,8 @@
   val the_proof: generic -> proof
   val map_theory: (theory -> theory) -> generic -> generic
   val map_proof: (proof -> proof) -> generic -> generic
+  val map_theory_result: (theory -> 'a * theory) -> generic -> 'a * generic
+  val map_proof_result: (proof -> 'a * proof) -> generic -> 'a * generic
   val theory_map: (generic -> generic) -> theory -> theory
   val proof_map: (generic -> generic) -> proof -> proof
   val theory_of: generic -> theory   (*total*)
@@ -496,6 +498,9 @@
 fun map_theory f = Theory o f o the_theory;
 fun map_proof f = Proof o f o the_proof;
 
+fun map_theory_result f = apsnd Theory o f o the_theory;
+fun map_proof_result f = apsnd Proof o f o the_proof;
+
 fun theory_map f = the_theory o f o Theory;
 fun proof_map f = the_proof o f o Proof;