src/Pure/ex/Def.thy

--- a/src/Pure/ex/Def.thy	Tue May 23 10:56:41 2023 +0200
+++ b/src/Pure/ex/Def.thy	Tue May 23 18:46:15 2023 +0200
@@ -41,7 +41,7 @@
 
 fun declare_def lhs eq lthy =
   let val def0: def = {lhs = lhs, eq = Thm.trim_context eq} in
-    lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
+    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)