chore: post-bootstrap cleanup

src/Lean/Elab/BindersUtil.lean

@@ -55,11 +55,10 @@ def expandMatchAlts? (stx : Syntax) : MacroM (Option Syntax) := do
 
 open TSyntax.Compat in
 def clearInMatchAlt (stx : TSyntax ``matchAlt) (vars : Array Ident) : TSyntax ``matchAlt :=
-  stx.1.modifyArg 3 fun rhs => Id.run do
+  stx.1.modifyArg 3 fun rhs => Unhygienic.run do
     let mut rhs := rhs
     for v in vars do
-      -- rhs ← `(clear% $v; $rhs)
-      rhs := mkNode `Lean.Parser.Term.clear #[mkAtom "clear%", v, mkNullNode, rhs]
+      rhs ← `(clear% $v; $rhs)
     return rhs
 
 def clearInMatch (stx : Syntax) (vars : Array Ident) : MacroM Syntax := do

src/Lean/Elab/Quotation.lean

@@ -583,12 +583,8 @@ abbrev IdxSet := HashSet Nat
 
 private partial def hasNoErrorIfUnused : Syntax → Bool
   | `(no_error_if_unused% $_) => true
-  -- | `(clear% $_; $body) => hasNoErrorIfUnused body
-  | stx =>
-    if stx.getKind == `Lean.Parser.Term.clear then
-      hasNoErrorIfUnused stx[3]
-    else
-      false
+  | `(clear% $_; $body) => hasNoErrorIfUnused body
+  | _ => false
 
 /--
 Given `rhss` the right-hand-sides of a `match`-syntax notation,