# HG changeset patch
# User wenzelm
# Date 1147898087 -7200
# Node ID d1a15431de34d65f155d648eeb1e691dc5dad227
# Parent  9d54d6d3bc2848d540b03c72d27de9d245680d58
added mapping;

diff -r 9d54d6d3bc28 -r d1a15431de34 src/Pure/context.ML
--- a/src/Pure/context.ML	Wed May 17 22:34:45 2006 +0200
+++ b/src/Pure/context.ML	Wed May 17 22:34:47 2006 +0200
@@ -73,6 +73,7 @@
   (*generic context*)
   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 the_theory: generic -> theory
   val the_proof: generic -> proof
   val map_theory: (theory -> theory) -> generic -> generic
@@ -582,6 +583,8 @@
 fun cases f _ (Theory thy) = f thy
   | cases _ g (Proof prf) = g prf;
 
+fun mapping f g = cases (Theory o f) (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;