diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index a09ded8a30..7f20864852 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -330,6 +330,11 @@ def elabMutual : CommandElab := fun stx => do
     Term.applyAttributes declName attrs
     for attrName in toErase do
       Attribute.erase declName attrName
+    if (← getEnv).isImportedConst declName && attrs.any (·.kind == .global) then
+      -- If an imported declaration is marked with a global attribute, there is no good way to track
+      -- its use generally and so Shake should conservatively preserve imports of the current
+      -- module.
+      recordExtraRevUseOfCurrentModule
 
 @[builtin_command_elab Lean.Parser.Command.«initialize»] def elabInitialize : CommandElab
   | stx@`($declModifiers:declModifiers $kw:initializeKeyword $[$id? : $type? ←]? $doSeq) => do
diff --git a/tests/lean/run/extraModUses.lean b/tests/lean/run/extraModUses.lean
index 908747de0e..eb2a53e4b7 100644
--- a/tests/lean/run/extraModUses.lean
+++ b/tests/lean/run/extraModUses.lean
@@ -174,7 +174,7 @@ attribute [grind =] List.append
 
 /--
 info: Entries: [import Init.Grind.Attr, public import Init.Prelude]
-Is rev mod use: false
+Is rev mod use: true
 -/
 #guard_msgs in #eval showExtraModUses