--- a/src/Pure/morphism.ML Sat Apr 14 00:46:20 2007 +0200
+++ b/src/Pure/morphism.ML Sat Apr 14 00:46:20 2007 +0200
@@ -37,6 +37,8 @@
val thm_morphism: (thm -> thm) -> morphism
val identity: morphism
val compose: morphism -> morphism -> morphism
+ val transform: morphism -> (morphism -> 'a) -> morphism -> 'a
+ val form: (morphism -> 'a) -> 'a
end;
structure Morphism: MORPHISM =
@@ -76,6 +78,9 @@
fun phi1 $> phi2 = compose phi2 phi1;
+fun transform phi f = fn psi => f (phi $> psi);
+fun form f = f identity;
+
end;
structure BasicMorphism: BASIC_MORPHISM = Morphism;