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
Mon, 15 May 2023 20:37:53 +0200
changeset 78059 d555983054f3
parent 78058 9de0d3d961d4
child 78060 b6c886b7184f
tuned;
src/Pure/Isar/class.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/class.ML	Mon May 15 20:23:42 2023 +0200
+++ b/src/Pure/Isar/class.ML	Mon May 15 20:37:53 2023 +0200
@@ -230,12 +230,11 @@
 fun activate_defs class thms thy =
   (case Element.eq_morphism thy thms of
     SOME eq_morph =>
-      fold (fn cls => fn thy =>
-        Context.theory_map
-          (Locale.amend_registration
-            {inst = (cls, base_morphism thy cls),
-              mixin = SOME (eq_morph, true),
-              export = export_morphism thy cls}) thy) (heritage thy [class]) thy
+      fold (fn cls => fn thy' =>
+        (Context.theory_map o Locale.amend_registration)
+         {inst = (cls, base_morphism thy' cls),
+          mixin = SOME (eq_morph, true),
+          export = export_morphism thy' cls} thy') (heritage thy [class]) thy
   | NONE => thy);
 
 fun register_operation class (c, t) input_only thy =
isabelle