diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 054e4a6f4b..e43c364ccc 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -181,14 +181,14 @@ where
     extra state, and return it. Otherwise, we just return `stx`. -/
   go : Syntax → StateT (Array Ident) MacroM Syntax
     | stx@`(($(_))) => pure stx
-    | `(·) => withFreshMacroScope do
-      let id : Ident ← `(a)
-      modify fun s => s.push id
+    | stx@`(·) => withFreshMacroScope do
+      let id ← mkFreshIdent stx (canonical := true)
+      modify (·.push id)
       pure id
     | stx => match stx with
-      | .node i k args => do
+      | .node _ k args => do
         let args ← args.mapM go
-        pure $ Syntax.node i k args
+        return .node (.fromRef stx (canonical := true)) k args
       | _ => pure stx
 
 /--
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 21a3da14ec..b08df63eed 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -600,7 +600,7 @@ def mkFreshBinderName [Monad m] [MonadQuotation m] : m Name :=
   Auxiliary method for creating a `Syntax.ident` containing
   a fresh name. This method is intended for creating fresh binder names.
   It is just a thin layer on top of `mkFreshUserName`. -/
-def mkFreshIdent [Monad m] [MonadQuotation m] (ref : Syntax) (canonical := false) : m Syntax :=
+def mkFreshIdent [Monad m] [MonadQuotation m] (ref : Syntax) (canonical := false) : m Ident :=
   return mkIdentFrom ref (← mkFreshBinderName) canonical
 
 private def applyAttributesCore
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index 892520a604..c212ad1fe8 100644
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/tests/lean/StxQuot.lean.expected.out
@@ -44,7 +44,7 @@ StxQuot.lean:19:15: error: expected term
 "#[(num \"1\"), [(num \"2\") (num \"3\")], (num \"4\")]"
 "#[(num \"2\")]"
 StxQuot.lean:95:39-95:44: error: unexpected antiquotation splice
-fun a => sorryAx (?m a) true : (a : ?m) → ?m a
+fun x => sorryAx (?m x) true : (x : ?m) → ?m x
 "#[(some 1), (some 2)]"
 StxQuot.lean:102:13-102:14: error: unknown identifier 'x' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check.
 "`id._@.UnhygienicMain._hyg.1"
diff --git a/tests/lean/diamond1.lean.expected.out b/tests/lean/diamond1.lean.expected.out
index 0a21f210b7..0416cad575 100644
--- a/tests/lean/diamond1.lean.expected.out
+++ b/tests/lean/diamond1.lean.expected.out
@@ -7,5 +7,5 @@ number of parameters: 1
 constructors:
 Foo.mk : {α : Type} → Bar (α → α) → (Bool → α) → Nat → Foo α
 def f : Nat → Foo Nat :=
-fun x => { toBar := { a := fun y => x + y, b := fun a a_1 => a + a_1 }, c := fun x_1 => x, d := x }
+fun x => { toBar := { a := fun y => x + y, b := fun x x_1 => x + x_1 }, c := fun x_1 => x, d := x }
 diamond1.lean:27:47-27:52: warning: field 'a' from 'Baz' has already been declared
diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean
index fbdc6194bd..d4afbd2a89 100644
--- a/tests/lean/interactive/hover.lean
+++ b/tests/lean/interactive/hover.lean
@@ -201,7 +201,7 @@ example : Nat := Id.run do (← 1)
 
 #check (· + ·)
       --^ textDocument/hover
-
+        --^ textDocument/hover
 macro "my_intro" x:(ident <|> "_") : tactic =>
   match x with
   | `($x:ident) => `(tactic| intro $x:ident)
diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out
index a33ab3c6e0..8654ab8f90 100644
--- a/tests/lean/interactive/hover.lean.expected.out
+++ b/tests/lean/interactive/hover.lean.expected.out
@@ -386,9 +386,15 @@ null
  "position": {"line": 201, "character": 8}}
 {"range":
  {"start": {"line": 201, "character": 8}, "end": {"line": 201, "character": 9}},
+ "contents": {"value": "```lean\n?m\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 201, "character": 10}}
+{"range":
+ {"start": {"line": 201, "character": 8},
+  "end": {"line": 201, "character": 13}},
  "contents":
  {"value":
-  "A placeholder for an implicit lambda abstraction's variable. The lambda abstraction is scoped to the surrounding parentheses.\nFor example, `(· + ·)` is equivalent to `fun x y => x + y`.\n",
+  "```lean\n?m x✝¹ x✝\n```\n***\n`a + b` computes the sum of `a` and `b`.\nThe meaning of this notation is type-dependent. ",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
  "position": {"line": 209, "character": 28}}
diff --git a/tests/lean/lambdaLiftCache.lean.expected.out b/tests/lean/lambdaLiftCache.lean.expected.out
index abbab55b88..6244068307 100644
--- a/tests/lean/lambdaLiftCache.lean.expected.out
+++ b/tests/lean/lambdaLiftCache.lean.expected.out
@@ -1,6 +1,6 @@
 [Compiler.saveMono] size: 1
-    def foo._lam_0 x a.1 : Nat :=
-      let _x.2 := Nat.add a.1 x;
+    def foo._lam_0 x x.1 : Nat :=
+      let _x.2 := Nat.add x.1 x;
       return _x.2
 [Compiler.saveMono] size: 2
     def foo x xs : List Nat :=