# HG changeset patch
# User wenzelm
# Date 1684612121 -7200
# Node ID 52d071212a7a660adb931df26b26424334885c3f
# Parent  3fde7a52c650621b698b239972df09284e6759e7
tuned;

diff -r 3fde7a52c650 -r 52d071212a7a src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Sat May 20 21:23:44 2023 +0200
+++ b/src/Pure/morphism.ML	Sat May 20 21:48:41 2023 +0200
@@ -187,8 +187,8 @@
 fun entity_set_context' ctxt a = entity_morphism (set_context' ctxt) a;
 fun entity_set_context'' context a = entity_morphism (set_context'' context) a;
 
-fun transform phi2 (Entity (f, phi1)) = Entity (f, phi1 $> phi2);
-fun transform_reset_context phi2 (Entity (f, phi1)) = Entity (f, reset_context (phi1 $> phi2));
+fun transform phi = entity_morphism (compose phi);
+fun transform_reset_context phi = entity_morphism (reset_context o compose phi);
 
 fun form (Entity (f, phi)) = f phi;
 fun form_entity f = f identity;