diff --git a/doc/tactics.md b/doc/tactics.md
index 6c7dfca37c..2598225316 100644
--- a/doc/tactics.md
+++ b/doc/tactics.md
@@ -244,7 +244,7 @@ theorem mem_split {a : α} {as : List α} (h : a ∈ as) : ∃ s t, as = s ++ a
   | cons b bs ih => cases h with
     | head a bs => exact ⟨[], ⟨bs, rfl⟩⟩
     | tail a b bs h =>
-      match bs, ih h with
+      match (generalizing := false) bs, ih h with
       | _, ⟨s, ⟨t, rfl⟩⟩ =>
         exists b::s; exists t
         rw [List.cons_append]