From 82497e3bcf882d92513bcead97249b60de08f55e Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 25 Dec 2020 22:58:33 +0100
Subject: [PATCH] fix: non-atomic identifiers in antiquotation splices

---
 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 bd885e2b32..c0a779ac5d 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -22,7 +22,7 @@ private partial def floatOutAntiquotTerms : Syntax → StateT (Syntax → TermEl
   | stx@(Syntax.node k args) => do
     if isAntiquot stx && !isEscapedAntiquot stx then
       let e := getAntiquotTerm stx
-      if !e.isIdent then
+      if !e.isIdent || !e.getId.isAtomic then
         return ← withFreshMacroScope do
           let a ← `(a)
           modify (fun cont stx => (`(let $a:ident := $e; $stx) : TermElabM _))