diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index 40c2c5f0f5..f5129192e8 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -890,7 +890,7 @@ def getMkMatcherInputInContext (matcherApp : MatcherApp) : MetaM MkMatcherInput
       fvarDecls := localDecls.toList
       patterns := patterns.toList : Match.AltLHS }
 
-  return { matcherName, matchType, discrInfos := mkArray matcherApp.discrs.size {}, lhss }
+  return { matcherName, matchType, discrInfos := matcherInfo.discrInfos, lhss }
 
 
 def withMkMatcherInput