diff -r ec817f4486b3 -r d7395ef81292 src/Pure/ex/Def.thy
--- a/src/Pure/ex/Def.thy	Mon May 15 14:09:45 2023 +0200
+++ b/src/Pure/ex/Def.thy	Mon May 15 14:10:44 2023 +0200
@@ -45,7 +45,9 @@
     val def: def = {lhs = lhs, mk_eq = fn phi => Morphism.thm phi eq0};
   in
     lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
-      (fn phi => (Data.map o Item_Net.update) (transform_def phi def))
+      (fn phi => fn context =>
+        let val psi = Morphism.transfer_morphism'' context $> phi $> Morphism.trim_context_morphism
+        in (Data.map o Item_Net.update) (transform_def psi def) context end)
   end;
 
 fun get_def ctxt ct =