diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Tools/functor.ML
--- a/src/HOL/Tools/functor.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Tools/functor.ML	Tue May 23 18:46:15 2023 +0200
@@ -263,7 +263,7 @@
         |> Local_Theory.note ((qualify identityN, []),
             [prove_identity lthy id_thm])
         |> snd
-        |> Local_Theory.declaration {syntax = false, pervasive = false}
+        |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
           (mapper_declaration comp_thm id_thm))
   in
     lthy