diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean
index ba2dd64855..66c453403c 100644
--- a/src/Init/Lean/Meta/Basic.lean
+++ b/src/Init/Lean/Meta/Basic.lean
@@ -314,10 +314,11 @@ do env ← getEnv;
    match env.find constName with
    | some (info@(ConstantInfo.thmInfo _)) =>
      condM reduceAll? (pure (some info)) (pure none)
-   | some info                            =>
+   | some (info@(ConstantInfo.defnInfo _)) =>
      condM reduceReducibleOnly?
        (condM (isReducible constName) (pure (some info)) (pure none))
        (pure (some info))
+   | some info => pure (some info)
    | none                                 =>
      if exception? then throwEx $ Exception.unknownConst constName
      else pure none