diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 03b792083a..5d10041a0b 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -100,12 +100,10 @@ private def elabParserMacroAux (prec : Syntax) (e : Syntax) : TermElabM Syntax :
   let (some declName) ← getDeclName?
     | throwError "invalid `leading_parser` macro, it must be used in definitions"
   match extractMacroScopes declName with
-  | { name := Name.str _ s _, scopes :=  scps, .. } =>
+  | { name := Name.str _ s _, .. } =>
     let kind := quote declName
     let s    := quote s
-    -- if the parser decl is hidden by hygiene, it doesn't make sense to provide an antiquotation kind
-    let antiquotKind ← if scps == [] then `(some $kind) else `(none)
-    ``(withAntiquot (mkAntiquot $s $antiquotKind) (leadingNode $kind $prec $e))
+    ``(withAntiquot (mkAntiquot $s $kind) (leadingNode $kind $prec $e))
   | _  => throwError "invalid `leading_parser` macro, unexpected declaration name"
 
 @[builtinTermElab «leading_parser»] def elabLeadingParserMacro : TermElab :=