diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index baf0051511..0f1c715cd0 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -679,9 +679,9 @@ syntax (name := delta) "delta" (ppSpace colGt ident)+ (location)? : tactic
 * `unfold id` unfolds definition `id`.
 * `unfold id1 id2 ...` is equivalent to `unfold id1; unfold id2; ...`.
 
-For non-recursive definitions, this tactic is identical to `delta`.
-For definitions by pattern matching, it uses "equation lemmas" which are
-autogenerated for each match arm.
+For non-recursive definitions, this tactic is identical to `delta`. For recursive definitions,
+it uses the "unfolding lemma" `id.eq_def`, which is generated for each recursive definition,
+to unfold according to the recursive definition given by the user.
 -/
 syntax (name := unfold) "unfold" (ppSpace colGt ident)+ (location)? : tactic