diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index c50b161f625e..e7a7322bf64a 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -794,8 +794,6 @@ partial def importModulesCore (imports : Array Import) : ImportStateM Unit := do
       continue
     modify fun s => { s with moduleNameSet := s.moduleNameSet.insert i.module }
     let mFile ← findOLean i.module
-    unless (← mFile.pathExists) do
-      throw <| IO.userError s!"object file '{mFile}' of module {i.module} does not exist"
     let (mod, region) ← readModuleData mFile
     importModulesCore mod.imports
     modify fun s => { s with
diff --git a/src/Lean/Util/Path.lean b/src/Lean/Util/Path.lean
index 90fd1875dc2e..70bdedd512dd 100644
--- a/src/Lean/Util/Path.lean
+++ b/src/Lean/Util/Path.lean
@@ -137,12 +137,17 @@ def initSearchPath (leanSysroot : FilePath) (sp : SearchPath := ∅) : IO Unit :
 private def initSearchPathInternal : IO Unit := do
   initSearchPath (← getBuildDir)
 
+/-- Returns the path of the .olean file for `mod` if it exists, or else throws an error. -/
 partial def findOLean (mod : Name) : IO FilePath := do
   let sp ← searchPathRef.get
-  if let some fname ← sp.findWithExt "olean" mod then
-    return fname
+  let pkg := mod.getRoot.toString (escape := false)
+  if let some root ← sp.findRoot "olean" pkg then
+    let path := modToFilePath root mod "olean"
+    if (← SearchPath.moduleExists root "olean" mod) then
+      return path
+    else
+      throw <| IO.userError s!"object file '{path}' of module {mod} does not exist"
   else
-    let pkg := FilePath.mk <| mod.getRoot.toString (escape := false)
     let mut msg := s!"unknown module prefix '{pkg}'
 
 No directory '{pkg}' or file '{pkg}.lean' in the search path entries: