# HG changeset patch
# User wenzelm
# Date 1165353285 -3600
# Node ID c86b761d6c066e0abc244ae66c1a49f13c32a948
# Parent  b8531e5164f074e8ea5b127d3b71ad41307b7b68
added mapping_result;

diff -r b8531e5164f0 -r c86b761d6c06 src/Pure/context.ML
--- a/src/Pure/context.ML	Tue Dec 05 22:14:44 2006 +0100
+++ b/src/Pure/context.ML	Tue Dec 05 22:14:45 2006 +0100
@@ -73,6 +73,7 @@
   datatype generic = Theory of theory | Proof of proof
   val cases: (theory -> 'a) -> (proof -> 'a) -> generic -> 'a
   val mapping: (theory -> theory) -> (proof -> proof) -> generic -> generic
+  val mapping_result: (theory -> 'a * theory) -> (proof -> 'a * proof) -> generic -> 'a * generic
   val the_theory: generic -> theory
   val the_proof: generic -> proof
   val map_theory: (theory -> theory) -> generic -> generic
@@ -582,6 +583,7 @@
   | cases _ g (Proof prf) = g prf;
 
 fun mapping f g = cases (Theory o f) (Proof o g);
+fun mapping_result f g = cases (apsnd Theory o f) (apsnd Proof o g);
 
 val the_theory = cases I (fn _ => raise Fail "Ill-typed context: theory expected");
 val the_proof = cases (fn _ => raise Fail "Ill-typed context: proof expected") I;