diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index b02e3bb34fd8..10b8e1cb88e0 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -178,8 +178,6 @@ where
           let r ← go sources (sourcesNew.push sourceNew)
           `(let __src := $source; $r)
 
-
-
 /--
 An *explicit source* is one of the structures `sᵢ` that appear in `{ s₁, …, sₙ with … }`.
 -/
@@ -244,7 +242,7 @@ private def isModifyOp? (stx : Syntax) : TermElabM (Option Syntax) := do
   let s? ← stx[2][0].getSepArgs.foldlM (init := none) fun s? arg => do
     /- arg is of the form `structInstField` -/
     if arg.getKind == ``Lean.Parser.Term.structInstField then
-      /- Remark: the syntax for `structInstField` (after expansion) is
+      /- Remark: the syntax for `structInstField` after macro expansion is
          ```
          def structInstLVal   := leading_parser (ident <|> numLit <|> structInstArrayRef) >> many (group ("." >> (ident <|> numLit)) <|> structInstArrayRef)
          def structInstField := leading_parser