# HG changeset patch
# User wenzelm
# Date 1137111182 -3600
# Node ID 5198a2c4c00e86192392edc313533f1903952d43
# Parent  ad7ae7870427bafaa32b2c847d80992bbbe98b48
added map_theory, map_proof;

diff -r ad7ae7870427 -r 5198a2c4c00e src/Pure/context.ML
--- a/src/Pure/context.ML	Fri Jan 13 01:13:00 2006 +0100
+++ b/src/Pure/context.ML	Fri Jan 13 01:13:02 2006 +0100
@@ -76,8 +76,10 @@
   val cases: (theory -> 'a) -> (proof -> 'a) -> generic -> 'a
   val the_theory: generic -> theory
   val the_proof: generic -> proof
-  val theory_of: generic -> theory
-  val proof_of: generic -> proof
+  val map_theory: (generic -> generic) -> theory -> theory
+  val map_proof: (generic -> generic) -> proof -> proof
+  val theory_of: generic -> theory   (*total*)
+  val proof_of: generic -> proof     (*total*)
 end;
 
 signature PRIVATE_CONTEXT =
@@ -579,6 +581,9 @@
 val the_theory = cases I (fn _ => raise Fail "Bad generic context: theory expected");
 val the_proof = cases (fn _ => raise Fail "Bad generic context: proof context expected") I;
 
+fun map_theory f = the_theory o f o Theory;
+fun map_proof f = the_proof o f o Proof;
+
 val theory_of = cases I theory_of_proof;
 val proof_of = cases init_proof I;