diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index 69c437031f..1e62b8e42d 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -665,13 +665,12 @@ universe u
 
 namespace Lean
 
-set_option linter.unusedVariables.funArgs false in
 /-- Typeclass used for presenting the output of an `#eval` command. -/
 class Eval (α : Type u) where
   -- We default `hideUnit` to `true`, but set it to `false` in the direct call from `#eval`
   -- so that `()` output is hidden in chained instances such as for some `IO Unit`.
   -- We take `Unit → α` instead of `α` because ‵α` may contain effectful debugging primitives (e.g., `dbg_trace`)
-  eval : (Unit → α) → forall (hideUnit : optParam Bool true), IO Unit
+  eval : (Unit → α) → (hideUnit : Bool := true) → IO Unit
 
 instance [ToString α] : Eval α where
   eval a _ := IO.println (toString (a ()))