diff -r bb85bda12b8e -r 90a43a9b3605 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Jun 06 15:29:43 2023 +0200
+++ b/src/Pure/Isar/code.ML	Tue Jun 06 21:02:37 2023 +0200
@@ -1307,9 +1307,11 @@
 
 (* abstract code declarations *)
 
-fun code_declaration strictness lift_phi f x =
-  Local_Theory.declaration {syntax = false, pervasive = false, pos = Position.thread_data ()}
-    (fn phi => Context.mapping (f strictness (lift_phi phi x)) I);
+fun code_declaration (strictness: strictness) transform f x =
+  let val x0 = transform Morphism.trim_context_morphism x in
+    Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
+      (fn phi => Context.mapping (f strictness (transform phi x0)) I)
+  end;
 
 
 (* types *)