diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index bf3e1bc542..0266342b14 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -324,7 +324,7 @@ syntax config := atomic("(" &"config") " := " term ")"
 syntax locationWildcard := "*"
 syntax locationHyp      := (colGt ident)+ ("⊢" <|> "|-")? -- TODO: delete
 syntax locationTargets  := (colGt ident)+ ("⊢" <|> "|-")?
-syntax location         := withPosition(" at " locationWildcard <|> locationHyp)
+syntax location         := withPosition(" at " (locationWildcard <|> locationHyp))
 
 syntax (name := change) "change " term (location)? : tactic
 syntax (name := changeWith) "change " term " with " term (location)? : tactic