diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean
index 49d5fa2087..5de5309387 100644
--- a/src/Lean/Parser/Do.lean
+++ b/src/Lean/Parser/Do.lean
@@ -94,7 +94,7 @@ def doIfCond    := withAntiquot (mkAntiquot "doIfCond" none (anonymous := false)
 def doForDecl := leading_parser termParser >> " in " >> withForbidden "do" termParser
 @[builtinDoElemParser] def doFor    := leading_parser "for " >> sepBy1 doForDecl ", " >> "do " >> doSeq
 
-def doMatchAlts := matchAlts (rhsParser := doSeq)
+def doMatchAlts := ppDedent <| matchAlts (rhsParser := doSeq)
 @[builtinDoElemParser] def doMatch := leading_parser:leadPrec "match " >> optional Term.generalizingParam >> sepBy1 matchDiscr ", " >> optType >> " with " >> doMatchAlts
 
 def doCatch      := leading_parser atomic ("catch " >> binderIdent) >> optional (" : " >> termParser) >> darrow >> doSeq
diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean
index 339eb4d78a..33a3086d2e 100644
--- a/src/Lean/Parser/Tactic.lean
+++ b/src/Lean/Parser/Tactic.lean
@@ -20,7 +20,7 @@ builtin_initialize
 
 def matchRhs  := Term.hole <|> Term.syntheticHole <|> tacticSeq
 def matchAlts := Term.matchAlts (rhsParser := matchRhs)
-@[builtinTacticParser] def «match» := leading_parser:leadPrec "match " >> optional Term.generalizingParam >> sepBy1 Term.matchDiscr ", " >> Term.optType >> " with " >> matchAlts
+@[builtinTacticParser] def «match» := leading_parser:leadPrec "match " >> optional Term.generalizingParam >> sepBy1 Term.matchDiscr ", " >> Term.optType >> " with " >> ppDedent matchAlts
 @[builtinTacticParser] def introMatch := leading_parser nonReservedSymbol "intro " >> matchAlts
 
 @[builtinTacticParser] def decide := leading_parser nonReservedSymbol "decide"
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 0dd669d99f..2ca3496630 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -133,7 +133,7 @@ def matchAlt (rhsParser : Parser := termParser) : Parser :=
 def matchAltExpr := matchAlt
 
 def matchAlts (rhsParser : Parser := termParser) : Parser :=
-  leading_parser ppDedent $ withPosition $ many1Indent (ppLine >> matchAlt rhsParser)
+  leading_parser withPosition $ many1Indent (ppLine >> matchAlt rhsParser)
 
 def matchDiscr := leading_parser optional (atomic (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> termParser
 
@@ -141,7 +141,7 @@ def trueVal  := leading_parser nonReservedSymbol "true"
 def falseVal := leading_parser nonReservedSymbol "false"
 def generalizingParam := leading_parser atomic ("(" >> nonReservedSymbol "generalizing") >> " := " >> (trueVal <|> falseVal)  >> ")"
 
-@[builtinTermParser] def «match» := leading_parser:leadPrec "match " >> optional generalizingParam >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts
+@[builtinTermParser] def «match» := leading_parser:leadPrec "match " >> optional generalizingParam >> sepBy1 matchDiscr ", " >> optType >> " with " >> ppDedent matchAlts
 @[builtinTermParser] def «nomatch» := leading_parser:leadPrec "nomatch " >> termParser
 
 def funImplicitBinder := atomic (lookahead ("{" >> many1 binderIdent >> (symbol " : " <|> "}"))) >> implicitBinder