Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/class.ML
changeset 78059 d555983054f3
parent 78041 1828b174768e
child 78060 b6c886b7184f 
--- 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