From c8bb2ea3cf72930bb060d10ddb0044c6ae3954d4 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Tue, 11 Oct 2022 13:00:23 -0700
Subject: [PATCH] chore: post-bootstrap cleanup

---
 src/Lean/Elab/BindersUtil.lean | 5 ++---
 src/Lean/Elab/Quotation.lean   | 8 ++------
 2 files changed, 4 insertions(+), 9 deletions(-)

diff --git a/src/Lean/Elab/BindersUtil.lean b/src/Lean/Elab/BindersUtil.lean
index b5c7ede4f6..dbf97fe1db 100644
--- a/src/Lean/Elab/BindersUtil.lean
+++ b/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
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 52b63bb7c7..399b72b8a3 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/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,