diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index 4f835ed8ed..027f229143 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -627,18 +627,19 @@ def mkSingletonDoSeq (doElem : Syntax) : Syntax :=
 /-
   If the given syntax is a `doIf`, return an equivalente `doIf` that has an `else` but no `else if`s or `let if`s.  -/
 private def expandDoIf? (stx : Syntax) : MacroM (Option Syntax) := match stx with
-  | `(doElem|if $cond then $t else $e) => pure none
-  | `(doElem|if $cond then $t $[else if $conds then $ts]* $[else $e?]?) => withRef stx do
+  | `(doElem|if $p:doIfProp then $t else $e) => pure none
+  | `(doElem|if $cond:doIfCond then $t $[else if $conds:doIfCond then $ts]* $[else $e?]?) => go cond t conds ts e?
+  | _ => pure none
+  where go cond t conds ts e? := withRef stx do
     let mut e      := e?.getD (← `(doSeq|pure PUnit.unit))
     let mut eIsSeq := true
     for (cond, t) in (conds.reverse.push cond).zip (ts.reverse.push t) do
       e ← if eIsSeq then e else `(doSeq|$e:doElem)
       e ← withRef cond <| match cond with
-        | `(doIfLet|let $pat := $d) => `(doElem|match $d:term with | $pat:term => $t | _ => $e)
-        | _                         => `(doElem|if $cond then $t else $e)
+        | `(doIfCond|let $pat := $d) => `(doElem|match $d:term with | $pat:term => $t | _ => $e)
+        | _                          => `(doElem|if $cond:doIfCond then $t else $e)
       eIsSeq := false
     return some e
-  | _ => pure none
 
 structure DoIfView where
   ref        : Syntax
diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean
index 2a64567f2a..9d449c5162 100644
--- a/src/Lean/Parser/Do.lean
+++ b/src/Lean/Parser/Do.lean
@@ -78,11 +78,13 @@ else if c_2 then
 ```
 -/
 def elseIf := atomic (group (withPosition (" else " >> checkLineEq >> " if ")))
-def doIfLet  := parser! "let " >> termParser >> " := " >> termParser
-def doIfCond := parser! optIdent >> termParser
+-- ensure `if $e then ...` still binds to `e:term`
+def doIfLet  := nodeWithAntiquot "doIfLet" `Lean.Parser.Term.doIfLet   <| "let " >> termParser >> " := " >> termParser
+def doIfProp := nodeWithAntiquot "doIfProp" `Lean.Parser.Term.doIfProp <| optIdent >> termParser
+def doIfCond := withAntiquot (mkAntiquot "doIfCond" none (anonymous := false)) <| doIfLet <|> doIfProp
 @[builtinDoElemParser] def doIf := parser! withPosition $
-  "if " >> (doIfLet <|> doIfCond) >> " then " >> doSeq
-  >> many (checkColGe "'else if' in 'do' must be indented" >> group (elseIf >> (doIfLet <|> doIfCond) >> " then " >> doSeq))
+  "if " >> doIfCond >> " then " >> doSeq
+  >> many (checkColGe "'else if' in 'do' must be indented" >> group (elseIf >> doIfCond >> " then " >> doSeq))
   >> optional (checkColGe "'else' in 'do' must be indented" >> " else " >> doSeq)
 @[builtinDoElemParser] def doUnless := parser! "unless " >> withForbidden "do" termParser >> "do " >> doSeq
 def doForDecl := parser! termParser >> " in " >> withForbidden "do" termParser
diff --git a/tests/lean/run/whileRepeat.lean b/tests/lean/run/whileRepeat.lean
index d0123e6a86..3f1f157383 100644
--- a/tests/lean/run/whileRepeat.lean
+++ b/tests/lean/run/whileRepeat.lean
@@ -17,7 +17,7 @@ syntax "while " termBeforeDo " do " doSeq : doElem
 
 macro_rules
   | `(doElem| while $cond do $seq) =>
-    `(doElem| repeat if $cond:term then $seq else break)
+    `(doElem| repeat if $cond then $seq else break)
 
 def test1 : IO Unit := do
   let mut i := 0
@@ -32,7 +32,7 @@ syntax "repeat " doSeq " until " term : doElem
 
 macro_rules
   | `(doElem| repeat $seq until $cond) =>
-    `(doElem| repeat do $seq; if $cond:term then break)
+    `(doElem| repeat do $seq; if $cond then break)
 
 def test2 : IO Unit := do
   let mut i := 0