diff --git a/src/Init/Lean/Elab/Util.lean b/src/Init/Lean/Elab/Util.lean
index d4bdbf5a45..6739cc4b7c 100644
--- a/src/Init/Lean/Elab/Util.lean
+++ b/src/Init/Lean/Elab/Util.lean
@@ -10,7 +10,7 @@ import Init.Lean.Parser
 namespace Lean
 
 def Syntax.prettyPrint (stx : Syntax) : Format :=
-match stx.reprint with -- TODO use syntax pretty printer
+match stx.truncateTrailing.reprint with -- TODO use syntax pretty printer
 | some str => format str.toFormat
 | none     => format stx
 
diff --git a/src/Init/Lean/Syntax.lean b/src/Init/Lean/Syntax.lean
index 46263d0f4d..2d6ff22b63 100644
--- a/src/Init/Lean/Syntax.lean
+++ b/src/Init/Lean/Syntax.lean
@@ -236,6 +236,11 @@ match setTailInfoAux info stx with
 | some stx => stx
 | none     => stx
 
+def truncateTrailing (stx : Syntax) : Syntax :=
+match stx.getTailInfo with
+| none      => stx
+| some info => stx.setTailInfo info.truncateTrailing
+
 private def reprintLeaf : Option SourceInfo → String → String
 -- no source info => add gracious amounts of whitespace to definitely separate tokens
 -- Note that the proper pretty printer does not use this function.