# HG changeset patch
# User wenzelm
# Date 1685094465 -7200
# Node ID b14421dc67598ed8f1481cff8211f542cd8f4907
# Parent  10487f6571bc7039c830c9b49ed0dd2dbff44c3b
clarified treatment of context;

diff -r 10487f6571bc -r b14421dc6759 src/Pure/ex/Def.thy
--- 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 =