diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index f2509edd85..bb01b19be3 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -350,15 +350,17 @@ def term.parenthesizer : CategoryParenthesizer | prec => do
   maybeParenthesize `term true wrapParens prec $
     parenthesizeCategoryCore `term prec
 where
-  /-- Wraps the term `stx` in parentheses and then copies its `SourceInfo` to the result.
-  The purpose of this is to copy synthetic delaborator positions from the `stx` node to the parentheses node,
-  which causes the info view to view both of these nodes as referring to the same expression.
-  If we did not copy info, the info view would consider the parentheses to belong to the outer term.
+  /-- Wraps the term `stx` in parentheses and then moves its `SourceInfo` to the result.
+  The purpose of this is to move synthetic delaborator positions from the `stx` node to the parentheses node,
+  which causes the info view to view the node with parentheses as referring to the parenthesized expression.
+  If we did not move info, the info view would consider the parentheses to belong to the outer term.
   Note: we do not do `withRef stx` because that causes the "(" and ")" tokens to have source info as well,
   causing the info view to highlight each parenthesis as an independent expression. -/
   wrapParens (stx : Syntax) : Syntax := Unhygienic.run do
+    let stxInfo := SourceInfo.fromRef stx
+    let stx := stx.setInfo .none
     let pstx ← `(($(⟨stx⟩)))
-    return pstx.raw.setInfo (SourceInfo.fromRef stx)
+    return pstx.raw.setInfo stxInfo
 
 @[builtin_category_parenthesizer tactic]
 def tactic.parenthesizer : CategoryParenthesizer | prec => do