diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 44f05ade78..a515882605 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -398,7 +398,7 @@ syntax locationWildcard := " *"
 A hypothesis location specification consists of 1 or more hypothesis references
 and optionally `⊢` denoting the goal.
 -/
-syntax locationHyp := (ppSpace colGt term:max)+ ppSpace patternIgnore( atomic("|" noWs "-") <|> "⊢")?
+syntax locationHyp := (ppSpace colGt term:max)+ patternIgnore(ppSpace (atomic("|" noWs "-") <|> "⊢"))?
 
 /--
 Location specifications are used by many tactics that can operate on either the
diff --git a/tests/lean/formatTerm.lean b/tests/lean/formatTerm.lean
index b8c9dfea54..f2a688fec8 100644
--- a/tests/lean/formatTerm.lean
+++ b/tests/lean/formatTerm.lean
@@ -63,3 +63,5 @@ def foo : a b c d e f g a b c d e f g h where
 #eval fmt `(calc
   1 = 1 := rfl
   1 = 1 := rfl)
+
+#eval fmt `(by rw [] at h)
diff --git a/tests/lean/formatTerm.lean.expected.out b/tests/lean/formatTerm.lean.expected.out
index 0928ad1263..5ef76fbd00 100644
--- a/tests/lean/formatTerm.lean.expected.out
+++ b/tests/lean/formatTerm.lean.expected.out
@@ -70,3 +70,4 @@ def foo✝ : a✝ b✝ c✝ d✝ e✝ f✝ g✝ a✝ b✝ c✝ d✝ e✝ f✝ g
 calc
   1 = 1 := rfl✝
   1 = 1 := rfl✝
+by rw [] at h✝
diff --git a/tests/lean/simp_trace.lean.expected.out b/tests/lean/simp_trace.lean.expected.out
index ec8d77ce13..816a8d9308 100644
--- a/tests/lean/simp_trace.lean.expected.out
+++ b/tests/lean/simp_trace.lean.expected.out
@@ -65,7 +65,7 @@ Try this: simp only [bla, h] at *
     | Sum.inl (y, z) => y + z
     | Sum.inr val => 0
 [Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x)
-Try this: simp only [bla, h] at h' 
+Try this: simp only [bla, h] at h'
 [Meta.Tactic.simp.rewrite] unfold bla, bla x ==> match h x with
     | Sum.inl (y, z) => y + z
     | Sum.inr val => 0