--- 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 =