diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 9eab27564e..e05790da44 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -454,6 +454,7 @@ where
 private def getIntrosSize : Expr → Nat
   | Expr.forallE _ _ b _ => getIntrosSize b + 1
   | Expr.letE _ _ _ b _  => getIntrosSize b + 1
+  | Expr.mdata _ b _     => getIntrosSize b
   | _                    => 0
 
 /- Recall that `ident' := ident <|> Term.hole` -/