diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 5adbed5a64..5964e6b29d 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -264,8 +264,13 @@ else do {
 
 @[combinatorFormatter symbol]
 def symbol.formatter (sym : String) : Formatter := do
-pushToken sym;
-goLeft
+stx ← getCur;
+if stx.isToken sym then do
+  pushToken sym;
+  goLeft
+else do
+  trace! `PrettyPrinter.format.backtrack ("unexpected syntax '" ++ stx ++ "', expected symbol '" ++ sym ++ "'");
+  throwBacktrack
 
 @[combinatorFormatter symbolNoWs] def symbolNoWs.formatter := symbol.formatter
 @[combinatorFormatter nonReservedSymbol] def nonReservedSymbol.formatter := symbol.formatter