diff --git a/src/Init/Lean/Syntax.lean b/src/Init/Lean/Syntax.lean
index 6d54e7847c..55ab07b8b6 100644
--- a/src/Init/Lean/Syntax.lean
+++ b/src/Init/Lean/Syntax.lean
@@ -284,7 +284,11 @@ match setTailInfoAux info stx with
 | none     => stx
 
 private def reprintLeaf : Option SourceInfo → String → String
-| none,      val => val
+-- no source info => add gracious amounts of whitespace to definitely separate tokens
+-- Note that the proper pretty printer does not use this function.
+-- The parser as well always produces source info, so round-tripping is still
+-- guaranteed.
+| none,      val => " " ++ val ++ " "
 | some info, val => info.leading.toString ++ val ++ info.trailing.toString
 
 partial def reprint : Syntax → Option String