src/Pure/Isar/bundle.ML

--- a/src/Pure/Isar/bundle.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/Pure/Isar/bundle.ML	Tue May 23 18:46:15 2023 +0200
@@ -129,7 +129,7 @@
       |> transform_bundle (Proof_Context.export_morphism ctxt' lthy)
       |> trim_context_bundle;
   in
-    lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
+    lthy |> Local_Theory.declaration {syntax = false, pervasive = true, pos = Binding.pos_of binding}
       (fn phi => fn context =>
         let val psi = Morphism.set_trim_context'' context phi
         in #2 (define_bundle (Morphism.binding psi binding, transform_bundle psi bundle) context) end)
@@ -181,9 +181,9 @@
     |> Attrib.local_notes kind facts
   end;
 
-fun bundle_declaration decl lthy =
+fun bundle_declaration pos decl lthy =
   lthy
-  |> (augment_target o Attrib.internal_declaration)
+  |> (augment_target o Attrib.internal_declaration pos)
     (Morphism.transform (Local_Theory.standard_morphism_theory lthy) decl)
   |> Generic_Target.standard_declaration (K true) decl;
 
@@ -198,10 +198,10 @@
      {define = bad_operation,
       notes = bundle_notes,
       abbrev = bad_operation,
-      declaration = K bundle_declaration,
+      declaration = fn {pos, ...} => bundle_declaration pos,
       theory_registration = bad_operation,
       locale_dependency = bad_operation,
-      pretty = pretty binding}
+      pretty = pretty binding};
 
 end;