diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean
index a0e45855f3..42a691e928 100644
--- a/src/Lean/Parser/Do.lean
+++ b/src/Lean/Parser/Do.lean
@@ -25,7 +25,8 @@ def doSeqIndent    := many1Indent $ doElemParser >> optional "; "
 def doSeqBracketed := parser! "{" >> sepBy1 doElemParser "; " true >> "}"
 def doSeq          := doSeqBracketed <|> doSeqIndent
 
-@[builtinDoElemParser] def doLet  := parser! "let " >> letDecl
+@[builtinDoElemParser] def doLet    := parser! "let " >> letDecl
+@[builtinDoElemParser] def doLetRec := parser! group ("let " >> nonReservedSymbol "rec ") >> letRecDecls
 def doId   := parser! «try» (ident >> optType >> leftArrow) >> termParser
 def doPat  := parser! «try» (termParser >> leftArrow) >> termParser >> optional (" | " >> termParser)
 @[builtinDoElemParser] def doLetArrow := parser! "let " >> (doId <|> doPat)
@@ -60,8 +61,8 @@ else if c_2 then
 ```
 -/
 @[builtinDoElemParser] def doIf := parser! withPosition $
-  "if " >> termParser >> " then " >> doSeq
-  >> many (checkColGe "'else if' in 'do' must be indented" >> «try» (" else " >> " if ") >> termParser >> " then " >> doSeq)
+  "if " >> optIdent >> termParser >> " then " >> doSeq
+  >> many (checkColGe "'else if' in 'do' must be indented" >> «try» (" else " >> " if ") >> optIdent >> termParser >> " then " >> doSeq)
   >> optional (checkColGe "'else' in 'do' must be indented" >> " else " >> doSeq)
 @[builtinDoElemParser] def doUnless := parser! "unless " >> termParser >> "do " >> doSeq
 @[builtinDoElemParser] def doFor    := parser! "for " >> termParser >> " in " >> termParser >> "do " >> doSeq
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 58e236f1e0..76433d1dc8 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -162,9 +162,9 @@ def attrArg : Parser := ident <|> strLit <|> numLit
 -- use `rawIdent` because of attribute names such as `instance`
 def attrInstance     := parser! rawIdent >> many attrArg
 def attributes       := parser! "@[" >> sepBy1 attrInstance ", " >> "]"
+def letRecDecls      := sepBy1 (group (optional «attributes» >> letDecl)) ", "
 @[builtinTermParser] def «letrec» :=
-    parser!:leadPrec withPosition (group ("let " >> nonReservedSymbol "rec ") >> sepBy1 (group (optional «attributes» >> letDecl)) ", ")
-                     >> optional "; " >> termParser
+    parser!:leadPrec withPosition (group ("let " >> nonReservedSymbol "rec ") >> letRecDecls) >> optional "; " >> termParser
 
 @[builtinTermParser] def nativeRefl   := parser! "nativeRefl! " >> termParser maxPrec
 @[builtinTermParser] def nativeDecide := parser! "nativeDecide! " >> termParser maxPrec