added mapping;
authorwenzelm
Wed May 17 22:34:47 2006 +0200 (2006-05-17)
changeset 19678d1a15431de34
parent 19677 9d54d6d3bc28
child 19679 ae4c1e2742c1
added mapping;
src/Pure/context.ML
     1.1 --- a/src/Pure/context.ML	Wed May 17 22:34:45 2006 +0200
     1.2 +++ b/src/Pure/context.ML	Wed May 17 22:34:47 2006 +0200
     1.3 @@ -73,6 +73,7 @@
     1.4    (*generic context*)
     1.5    datatype generic = Theory of theory | Proof of proof
     1.6    val cases: (theory -> 'a) -> (proof -> 'a) -> generic -> 'a
     1.7 +  val mapping: (theory -> theory) -> (proof -> proof) -> generic -> generic
     1.8    val the_theory: generic -> theory
     1.9    val the_proof: generic -> proof
    1.10    val map_theory: (theory -> theory) -> generic -> generic
    1.11 @@ -582,6 +583,8 @@
    1.12  fun cases f _ (Theory thy) = f thy
    1.13    | cases _ g (Proof prf) = g prf;
    1.14  
    1.15 +fun mapping f g = cases (Theory o f) (Proof o g);
    1.16 +
    1.17  val the_theory = cases I (fn _ => raise Fail "Ill-typed context: theory expected");
    1.18  val the_proof = cases (fn _ => raise Fail "Ill-typed context: proof expected") I;
    1.19