diff --git a/src/Lean/Compiler/IR/Checker.lean b/src/Lean/Compiler/IR/Checker.lean
index 6a60d3dd11..0b55cd354f 100644
--- a/src/Lean/Compiler/IR/Checker.lean
+++ b/src/Lean/Compiler/IR/Checker.lean
@@ -82,8 +82,6 @@ def checkScalarVar (x : VarId) : M Unit :=
   checkVarType x IRType.isScalar
 
 def checkFullApp (c : FunId) (ys : Array Arg) : M Unit := do
-  if c == `hugeFuel then
-    throw "the auxiliary constant `hugeFuel` cannot be used in code, it is used internally for compiling `partial` definitions"
   let decl ← getDecl c
   unless ys.size == decl.params.size do
     throw s!"incorrect number of arguments to '{c}', {ys.size} provided, {decl.params.size} expected"