Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Sat, 20 May 2023 21:48:41 +0200
changeset 78089 52d071212a7a
parent 78088 3fde7a52c650
child 78090 79ad3181071b
tuned;
src/Pure/morphism.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle