src/Pure/context.ML
changeset 26486 b65a5272b360
parent 26463 9283b4185fdf
child 26623 81547c8d51f8
     1.1 --- a/src/Pure/context.ML	Sat Mar 29 19:14:07 2008 +0100
     1.2 +++ b/src/Pure/context.ML	Sat Mar 29 19:14:08 2008 +0100
     1.3 @@ -57,6 +57,8 @@
     1.4    val the_proof: generic -> proof
     1.5    val map_theory: (theory -> theory) -> generic -> generic
     1.6    val map_proof: (proof -> proof) -> generic -> generic
     1.7 +  val map_theory_result: (theory -> 'a * theory) -> generic -> 'a * generic
     1.8 +  val map_proof_result: (proof -> 'a * proof) -> generic -> 'a * generic
     1.9    val theory_map: (generic -> generic) -> theory -> theory
    1.10    val proof_map: (generic -> generic) -> proof -> proof
    1.11    val theory_of: generic -> theory   (*total*)
    1.12 @@ -496,6 +498,9 @@
    1.13  fun map_theory f = Theory o f o the_theory;
    1.14  fun map_proof f = Proof o f o the_proof;
    1.15  
    1.16 +fun map_theory_result f = apsnd Theory o f o the_theory;
    1.17 +fun map_proof_result f = apsnd Proof o f o the_proof;
    1.18 +
    1.19  fun theory_map f = the_theory o f o Theory;
    1.20  fun proof_map f = the_proof o f o Proof;
    1.21