diff --git a/src/Lean/Compiler/Util.lean b/src/Lean/Compiler/Util.lean
index 3bf806cf3a..76e67f585c 100644
--- a/src/Lean/Compiler/Util.lean
+++ b/src/Lean/Compiler/Util.lean
@@ -74,6 +74,7 @@ private def getDeclNamesForCodeGen : Declaration → List Name
   | Declaration.defnDecl { name := n, .. }   => [n]
   | Declaration.mutualDefnDecl defs          => defs.map fun d => d.name
   | Declaration.opaqueDecl { name := n, .. } => [n]
+  | Declaration.axiomDecl { name := n, .. }  => [n] -- axiom may be tagged with `@[extern ...]`
   | _                                        => []
 
 def checkIsDefinition (env : Environment) (n : Name) : Except String Unit :=
diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 40465032ea..1003aaeb84 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -82,6 +82,8 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
       Term.ensureNoUnassignedMVars decl
       addDecl decl
       Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterTypeChecking
+      if isExtern (← getEnv) declName then
+        compileDecl decl
       Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterCompilation
 
 /-