fix: pattern variables cannot shadow each other

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -188,9 +188,15 @@ private def skippingBinders {α} (numParams : Nat) (x : Array Name → DelabM α
 where
   loop : Nat → Array Name → DelabM α
     | 0,   varNames => x varNames
-    | n+1, varNames =>
-      withBindingBodyUnusedName fun id => do
-        loop n (varNames.push id.getId)
+    | n+1, varNames => do
+      let varName ← (← getExpr).bindingName!.eraseMacroScopes
+      -- Pattern variables cannot shadow each other
+      if varNames.contains varName then
+        let varName := (← getLCtx).getUnusedName varName
+        loop n (varNames.push varName)
+      else
+        withBindingBodyUnusedName fun id => do
+          loop n (varNames.push id.getId)
 
 /--
   Delaborate applications of "matchers" such as

tests/lean/match1.lean.expected.out

@@ -34,7 +34,7 @@ fun (x : Nat × Nat) =>
 fun (x x_1 : Option Nat) =>
   match x, x_1 with 
   | some a, some b => some (a + b)
-  | x, x => none : Option Nat → Option Nat → Option Nat
+  | x, x_2 => fun (x : Option Nat) => none : Option Nat → Option Nat → Option Nat
 fun (x : Nat) =>
   (match x with 
     | 0 => id