# HG changeset patch
# User wenzelm
# Date 1684175873 -7200
# Node ID d555983054f307fe5ac63d171d33d125c22e33c0
# Parent  9de0d3d961d40eea28078d92bf8ae81e1607a231
tuned;

diff -r 9de0d3d961d4 -r d555983054f3 src/Pure/Isar/class.ML
--- 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 =