diff --git a/src/Lean/Linter.lean b/src/Lean/Linter.lean
index 0b8c74d0ca..323bb26d14 100644
--- a/src/Lean/Linter.lean
+++ b/src/Lean/Linter.lean
@@ -11,7 +11,7 @@ import Lean.Message
 
 namespace Lean
 
-def Linter := Environment → Name → /-Syntax → -/IO MessageLog
+def Linter := Environment → Name → Syntax → IO MessageLog
 
 def mkLintersRef : IO (IO.Ref (Array Linter)) :=
 IO.mkRef #[]
diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp
index 686d196ca6..81d3a5b569 100644
--- a/src/frontends/lean/definition_cmds.cpp
+++ b/src/frontends/lean/definition_cmds.cpp
@@ -480,7 +480,7 @@ static environment elab_single_def(parser & p, decl_cmd_kind const & kind, cmd_m
         lean_assert(io_result_is_ok(r.raw()));
         array_ref<object *> linters(io_result_get_value(r.raw()), true);
         for (object * const & linter : linters) {
-            object * r2 = apply_3(linter, new_env.to_obj_arg(), local_name_p(fn).to_obj_arg(), io_mk_world());
+            object * r2 = apply_4(linter, new_env.to_obj_arg(), local_name_p(fn).to_obj_arg(), lean_box(0) /* Syntax.missing */, io_mk_world());
             consume_io_result(r2);
         }
 
diff --git a/tests/plugin/SnakeLinter.lean b/tests/plugin/SnakeLinter.lean
index 656f3aef42..6be20fad34 100644
--- a/tests/plugin/SnakeLinter.lean
+++ b/tests/plugin/SnakeLinter.lean
@@ -5,7 +5,7 @@ open Lean
 def oh_no : Nat := 0
 
 def snakeLinter : Linter :=
-fun env n =>
+fun env n stx =>
   -- TODO(Sebastian): return actual message with position from syntax tree
   if n.toString.contains '_' then throw $ IO.userError "SNAKES!!"
   else pure MessageLog.empty