src/Pure/context.ML
changeset 18665 5198a2c4c00e
parent 18632 3149c6abe876
child 18678 dd0c569fa43d
     1.1 --- a/src/Pure/context.ML	Fri Jan 13 01:13:00 2006 +0100
     1.2 +++ b/src/Pure/context.ML	Fri Jan 13 01:13:02 2006 +0100
     1.3 @@ -76,8 +76,10 @@
     1.4    val cases: (theory -> 'a) -> (proof -> 'a) -> generic -> 'a
     1.5    val the_theory: generic -> theory
     1.6    val the_proof: generic -> proof
     1.7 -  val theory_of: generic -> theory
     1.8 -  val proof_of: generic -> proof
     1.9 +  val map_theory: (generic -> generic) -> theory -> theory
    1.10 +  val map_proof: (generic -> generic) -> proof -> proof
    1.11 +  val theory_of: generic -> theory   (*total*)
    1.12 +  val proof_of: generic -> proof     (*total*)
    1.13  end;
    1.14  
    1.15  signature PRIVATE_CONTEXT =
    1.16 @@ -579,6 +581,9 @@
    1.17  val the_theory = cases I (fn _ => raise Fail "Bad generic context: theory expected");
    1.18  val the_proof = cases (fn _ => raise Fail "Bad generic context: proof context expected") I;
    1.19  
    1.20 +fun map_theory f = the_theory o f o Theory;
    1.21 +fun map_proof f = the_proof o f o Proof;
    1.22 +
    1.23  val theory_of = cases I theory_of_proof;
    1.24  val proof_of = cases init_proof I;
    1.25