diff --git a/src/Lean/Compiler/IR/ToIR.lean b/src/Lean/Compiler/IR/ToIR.lean
index e395f4920395..257f40684e19 100644
--- a/src/Lean/Compiler/IR/ToIR.lean
+++ b/src/Lean/Compiler/IR/ToIR.lean
@@ -214,19 +214,15 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
                 | none => lowerCode k
               loop 0 0
             return .vdecl objVar type (.ctor ctorInfo objArgs) (← lowerNonObjectFields ())
-      | some (.axiomInfo ..) =>
-        throwNamedError lean.dependsOnNoncomputable f!"axiom '{name}' not supported by code generator; consider marking definition as 'noncomputable'"
-      | some (.quotInfo ..) =>
-        throwError f!"quot {name} unsupported by code generator"
       | some (.defnInfo ..) | some (.opaqueInfo ..) =>
         if let some code ← tryIrDecl? name irArgs then
           return code
         else
           mkExpr (.fap name irArgs)
+      | some (.axiomInfo ..) | .some (.quotInfo ..) | .some (.inductInfo ..) | .some (.thmInfo ..) =>
+        throwNamedError lean.dependsOnNoncomputable f!"'{name}' not supported by code generator; consider marking definition as 'noncomputable'"
       | some (.recInfo ..) =>
         throwError f!"code generator does not support recursor '{name}' yet, consider using 'match ... with' and/or structural recursion"
-      | some (.inductInfo ..) => panic! "induct unsupported by code generator"
-      | some (.thmInfo ..) => panic! "thm unsupported by code generator"
       | none => panic! "reference to unbound name"
   | .fvar fvarId args =>
     match (← get).fvars[fvarId]? with
diff --git a/tests/lean/496.lean.expected.out b/tests/lean/496.lean.expected.out
index 8612fcef9790..f100258863a3 100644
--- a/tests/lean/496.lean.expected.out
+++ b/tests/lean/496.lean.expected.out
@@ -1,2 +1,2 @@
-496.lean:3:4-3:8: error(lean.dependsOnNoncomputable): axiom 'foo' not supported by code generator; consider marking definition as 'noncomputable'
+496.lean:3:4-3:8: error(lean.dependsOnNoncomputable): 'foo' not supported by code generator; consider marking definition as 'noncomputable'
 496.lean:9:4-9:8: error(lean.dependsOnNoncomputable): failed to compile definition, consider marking it as 'noncomputable' because it depends on 'bla1', which is 'noncomputable'