src/Pure/Isar/class.ML

--- a/src/Pure/Isar/class.ML	Tue May 16 17:08:31 2023 +0200
+++ b/src/Pure/Isar/class.ML	Tue May 16 19:20:18 2023 +0200
@@ -157,8 +157,9 @@
 val base_morphism = #base_morph oo the_class_data;
 
 fun morphism thy class =
-  base_morphism thy class $>
-  Morphism.default (Element.eq_morphism thy (these_defs thy [class]));
+  Morphism.set_context thy
+   (base_morphism thy class $>
+    Morphism.default (Element.eq_morphism (these_defs thy [class])));
 
 val export_morphism = #export_morph oo the_class_data;
 
@@ -230,7 +231,7 @@
   in Class_Data.map add_class thy end;
 
 fun activate_defs class thms thy =
-  (case Element.eq_morphism thy thms of
+  (case Element.eq_morphism thms of
     SOME eq_morph =>
       fold (fn cls => fn thy' =>
         (Context.theory_map o Locale.amend_registration)
@@ -359,7 +360,8 @@
 
 fun target_const class phi0 prmode (b, rhs) lthy =
   let
-    val export = Variable.export_morphism lthy (Local_Theory.target_of lthy);
+    val export =
+      Morphism.set_context' lthy (Variable.export_morphism lthy (Local_Theory.target_of lthy));
     val guess_identity = guess_morphism_identity (b, rhs) export;
     val guess_canonical = guess_morphism_identity (b, rhs) (export $> phi0);
   in