--- a/src/Pure/Isar/method.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/Pure/Isar/method.ML	Tue May 23 18:46:15 2023 +0200
@@ -608,7 +608,8 @@
                 val facts =
                   Attrib.partial_evaluation ctxt [((Binding.name "dummy", []), thms)]
                   |> map (fn (_, bs) =>
-                    ((Binding.empty, [Attrib.internal (K attribute)]), Attrib.trim_context_thms bs));
+                    ((Binding.empty, [Attrib.internal pos (K attribute)]),
+                      Attrib.trim_context_thms bs));
 
                 val decl =
                   Morphism.entity (fn phi => fn context =>