From 4b78d02a5ea6c7625227ea65d9824967b1a9d16f Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 28 Apr 2022 22:39:52 +0200
Subject: [PATCH] fix: do not discriminate anonymous antiquots after all

---
 src/Lean/Elab/Quotation.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 9cf19878d2..d6994d609c 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -323,7 +323,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
       --   let id := stx; let e := stx; ...
       -- else
       --   let e := stx; ...
-      if pseudoKinds.all id then unconditionally rhsFn else pure {
+      if (getCanonicalAntiquot quoted)[3].isNone || pseudoKinds.all id then unconditionally rhsFn else pure {
         check   := shape ks none,
         onMatch := fun
           | other _ => undecided