From 9ec583e808ef5441780bede92b1320255aaa1e96 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 8 Oct 2020 13:54:49 -0700
Subject: [PATCH] chore: use `(doElem| ...)` quotation instead of `auxDo` idiom

---
 src/Lean/Elab/Do.lean | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index 39a376ce59..bc034abcb8 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -209,8 +209,7 @@ hasExitPointPred (fun c => !isTerminalAction c) c
 def mkAuxDeclFor {m} [Monad m] [MonadQuotation m] (e : Syntax) (mkCont : Syntax → m Code) : m Code := withFreshMacroScope do
 y ← `(y);
 let yName := y.getId;
-auxDo ← `(do let y ← $e:term);
-let doElem := (getDoSeqElems (getDoSeq auxDo)).head!;
+doElem ← `(doElem| let y ← $e:term);
 -- Add elaboration hint for producing sane error message
 y ← `(ensureExpectedType! "type mismatch, result value" $y);
 k ← mkCont y;
@@ -960,9 +959,8 @@ private partial def expandLiftMethodAux : Syntax → StateT (List Syntax) MacroM
   else if k == `Lean.Parser.Term.liftMethod then withFreshMacroScope $ do
     let term := args.get! 1;
     term ← expandLiftMethodAux term;
-    auxDo ← `(do let a ← $term:term);
-    let auxDoElems := getDoSeqElems (getDoSeq auxDo);
-    modify fun s => s ++ auxDoElems;
+    auxDoElem ← `(doElem| let a ← $term:term);
+    modify fun s => s ++ [auxDoElem];
     `(a)
   else do
     args ← args.mapM expandLiftMethodAux;