diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean
index 0ff185de59..c96b3c0fbd 100644
--- a/src/Lean/AddDecl.lean
+++ b/src/Lean/AddDecl.lean
@@ -148,8 +148,12 @@ where
           let env ← (← getEnv).addDeclAux (← getOptions) decl (← read).cancelTk?
             |> ofExceptKernelException
           setEnv env
-          for n in decl.getTopLevelNames do
-            registerAxiomsForDecl n
+          if env.header.isModule then
+            -- Under the module system, must record axioms in environment extension now when we
+            -- still have access to the declaration's body. We could skip this for non-opaque decls
+            -- but for them, registering simply acts as a cache.
+            for n in decl.getTopLevelNames do
+              registerAxiomsForDecl n
         catch ex =>
           -- avoid follow-up errors by (trying to) add broken decl as axiom
           addAsAxiom
diff --git a/src/Lean/Util/CollectAxioms.lean b/src/Lean/Util/CollectAxioms.lean
index 50975a554a..26a8cc2125 100644
--- a/src/Lean/Util/CollectAxioms.lean
+++ b/src/Lean/Util/CollectAxioms.lean
@@ -51,6 +51,10 @@ def collectAxioms [Monad m] [MonadEnv m] (constName : Name) : m (Array Name) :=
   let (_, s) := ((CollectAxioms.collect constName).run env).run {}
   pure s.axioms
 
+/--
+Registers axioms used by the declaration in an environment extension so they can be retrieved even
+if some parts of the declaration's become inaccessible.
+-/
 def registerAxiomsForDecl (n : Name) : CoreM Unit := do
   let axioms ← collectAxioms n
   modifyEnv (exportedAxiomsExt.addEntry · (n, axioms))