src/Pure/Isar/interpretation.ML

--- a/src/Pure/Isar/interpretation.ML	Tue Jul 25 12:27:31 2023 +0200
+++ b/src/Pure/Isar/interpretation.ML	Tue Jul 25 14:12:26 2023 +0200
@@ -111,7 +111,7 @@
     fun register (dep, eqns) ctxt =
       ctxt |> add_registration
         {inst = dep,
-          mixin = Option.map (rpair true) (Element.eq_morphism (eqns @ eqns')),
+          mixin = Option.map (rpair true) (Element.eq_morphism ctxt (eqns @ eqns')),
           export = export};
   in ctxt'' |> fold register (deps' ~~ eqnss') end;