diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index dba40bc3dd..2bfddb34ba 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -175,7 +175,7 @@ def matchAltsWhereDecls := parser! matchAlts >> optional whereDecls
 
 @[builtinTermParser] def noindex := parser! "noindex!" >> termParser maxPrec
 
-@[builtinTermParser] def binrel  := parser! "binrel!" >> ident >> termParser maxPrec >> termParser maxPrec
+@[builtinTermParser] def binrel  := parser! "binrel! " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
 
 @[builtinTermParser] def typeOf             := parser! "typeOf! " >> termParser maxPrec
 @[builtinTermParser] def ensureTypeOf       := parser! "ensureTypeOf! " >> termParser maxPrec >> strLit >> termParser
diff --git a/tests/lean/macroStack.lean.expected.out b/tests/lean/macroStack.lean.expected.out
index 48c1949577..3753785189 100644
--- a/tests/lean/macroStack.lean.expected.out
+++ b/tests/lean/macroStack.lean.expected.out
@@ -1,7 +1,7 @@
 macroStack.lean:4:5: error: unknown identifier 'x'
 macroStack.lean:8:6: error: unknown identifier 'x'
 with resulting expansion
-  binrel! Greater✝x 0
+  binrel! Greater✝ x 0
 while expanding
   x > 0
 while expanding