# 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;