diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean
index b16b4ecb6c..7fd57d4cbd 100644
--- a/src/Init/Lean/Parser/Parser.lean
+++ b/src/Init/Lean/Parser/Parser.lean
@@ -444,7 +444,8 @@ fun c s =>
   let pos := s.pos;
   let s   := p c s;
   if s.hasError then
-    if pOpt then
+    if s.pos > pos then s
+    else if pOpt then
       let s := s.restore sz pos;
       if s.stackSize - iniSz == 2 && unboxSingleton then
         s.popSyntax