diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index 4e41424674..a5ee409bca 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -69,7 +69,7 @@ private def mkHintBody (cs : Array Syntax) (p : Syntax) : MacroM Syntax := do
   return body
 
 macro_rules
-  | `(unif_hint $bs* where $cs* |- $p) => do
+  | `(unif_hint $bs:explicitBinder* where $cs* |- $p) => do
     let body ← mkHintBody cs p
     `(@[unificationHint] def hint $bs:explicitBinder* : Sort _ := $body)
   | `(unif_hint $n:ident $bs* where $cs* |- $p) => do