diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index 4dec7d6d9c..39a376ce59 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -1208,8 +1208,11 @@ partial def doSeqToCode : List Syntax → M CodeBlock
         pure $ mkTerminalAction term
       else
         mkSeq term <$> doSeqToCode doElems
-    else
-      throwError ("unexpected do-element" ++ Format.line ++ toString doElem)
+    else do
+      doElem? ← liftMacroM $ expandMacro? doElem;
+      match doElem? with
+      | some doElem => doSeqToCode (doElem::doElems)
+      | none => throwError ("unexpected do-element" ++ Format.line ++ toString doElem)
 
 def run (doStx : Syntax) (m : Syntax) : TermElabM CodeBlock :=
 (doSeqToCode $ getDoSeqElems $ getDoSeq doStx).run { ref := doStx, m := m }
diff --git a/tests/lean/run/doNotation3.lean b/tests/lean/run/doNotation3.lean
index 53dd203152..241222c721 100644
--- a/tests/lean/run/doNotation3.lean
+++ b/tests/lean/run/doNotation3.lean
@@ -56,3 +56,15 @@ unless (← g 0 1 (← IO.mkRef (10, 20))) == (10, 20) do throw $ IO.userError "
 return ()
 
 #eval gTest
+
+macro "ret!" x:term : doElem => `(return $x)
+
+def f1 (x : Nat) : Nat := do
+if x == 0 then
+  ret! 100
+x := x + 1
+ret! x
+
+theorem ex1 : f1 0 = 100 := rfl
+theorem ex2 : f1 1 = 2 := rfl
+theorem ex3 : f1 3 = 4 := rfl