diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index 163fe85d1a..0c9ae5a452 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -103,6 +103,8 @@ def mkPPContext (nCtx : NamingContext) (ctx : MessageDataContext) : PPContext :=
 }
 
 def ofSyntax (stx : Syntax) : MessageData :=
+  -- discard leading/trailing whitespace
+  let stx := stx.copyHeadTailInfoFrom .missing
   .ofPPFormat {
     pp := fun
       | some ctx => ppTerm ctx ⟨stx⟩  -- HACK: might not be a term