diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index bd21bab657..1687eea006 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -272,32 +272,31 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
     else if isAntiquot quoted && !isEscapedAntiquot quoted then
       -- quotation contains a single antiquotation
       let k := antiquotKind? quoted |>.get!
-      match getAntiquotTerm quoted with
-      | `(_) => unconditionally pure
-      | `($id:ident) =>
-        -- Antiquotation kinds like `$id:ident` influence the parser, but also need to be considered by
-        -- `match` (but not by quotation terms). For example, `($id:ident) and `($e) are not
-        -- distinguishable without checking the kind of the node to be captured. Note that some
-        -- antiquotations like the latter one for terms do not correspond to any actual node kind
-        -- (signified by `k == Name.anonymous`), so we would only check for `ident` here.
-        --
-        -- if stx.isOfKind `ident then
-        --   let id := stx; let e := stx; ...
-        -- else
-        --   let e := stx; ...
-        let rhsFn := (`(let $id := discr; $(·)))
-        if k == Name.anonymous then unconditionally rhsFn else pure {
-          check   := shape k none,
-          onMatch := fun
-            | other _ => undecided
-            | taken@(shape k' sz) =>
-              if k' == k then
-                covered (adaptRhs rhsFn ∘ noOpMatchAdaptPats taken) (exhaustive := sz.isNone)
-              else uncovered
-            | _ => uncovered,
-          doMatch := fun yes no => do `(cond (Syntax.isOfKind discr $(quote k)) $(← yes []) $(← no)),
-        }
-      | anti => throwErrorAt anti "unsupported antiquotation kind in pattern"
+      let rhsFn := match getAntiquotTerm quoted with
+        | `(_)         => pure
+        | `($id:ident) => fun stx => `(let $id := discr; $(stx))
+        | anti =>         fun _   => throwErrorAt anti "unsupported antiquotation kind in pattern"
+      -- Antiquotation kinds like `$id:ident` influence the parser, but also need to be considered by
+      -- `match` (but not by quotation terms). For example, `($id:ident) and `($e) are not
+      -- distinguishable without checking the kind of the node to be captured. Note that some
+      -- antiquotations like the latter one for terms do not correspond to any actual node kind
+      -- (signified by `k == Name.anonymous`), so we would only check for `ident` here.
+      --
+      -- if stx.isOfKind `ident then
+      --   let id := stx; let e := stx; ...
+      -- else
+      --   let e := stx; ...
+      if k == Name.anonymous then unconditionally rhsFn else pure {
+        check   := shape k none,
+        onMatch := fun
+          | other _ => undecided
+          | taken@(shape k' sz) =>
+            if k' == k then
+              covered (adaptRhs rhsFn ∘ noOpMatchAdaptPats taken) (exhaustive := sz.isNone)
+            else uncovered
+          | _ => uncovered,
+        doMatch := fun yes no => do `(cond (Syntax.isOfKind discr $(quote k)) $(← yes []) $(← no)),
+      }
     else if isAntiquotSuffixSplice quoted then throwErrorAt quoted "unexpected antiquotation splice"
     else if isAntiquotSplice quoted then throwErrorAt quoted "unexpected antiquotation splice"
     else if quoted.getArgs.size == 1 && isAntiquotSuffixSplice quoted[0] then