clarified treatment of context;

--- a/src/Pure/ex/Def.thy	Fri May 26 11:46:51 2023 +0200
+++ b/src/Pure/ex/Def.thy	Fri May 26 11:47:45 2023 +0200
@@ -32,6 +32,9 @@
 fun transform_def phi ({lhs, eq}: def) =
   {lhs = Morphism.term phi lhs, eq = Morphism.thm phi eq};
 
+fun trim_context_def ({lhs, eq}: def) =
+  {lhs = lhs, eq = Thm.trim_context eq};
+
 structure Data = Generic_Data
 (
   type T = def Item_Net.T;
@@ -43,8 +46,8 @@
   let val def0: def = {lhs = lhs, eq = Thm.trim_context eq} in
     lthy |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
       (fn phi => fn context =>
-        let val psi = Morphism.set_trim_context'' context phi
-        in (Data.map o Item_Net.update) (transform_def psi def0) context end)
+        let val def' = def0 |> transform_def phi |> trim_context_def
+        in (Data.map o Item_Net.update) def' context end)
   end;
 
 fun get_def ctxt ct =