diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean
index d29c2e3a9a..09d92ae39b 100644
--- a/library/init/meta/simp_tactic.lean
+++ b/library/init/meta/simp_tactic.lean
@@ -17,7 +17,7 @@ meta_constant simp_lemmas : Type₁
    computed with respect to the given transparency setting. -/
 meta_constant mk_simp_lemmas_core     : transparency → list name → list name → tactic simp_lemmas
 /- Create an empty simp_lemmas. That is, it ignores the lemmas marked with the [simp] attribute.  -/
-meta_constant mk_empy_simp_lemmas     : tactic simp_lemmas
+meta_constant mk_empty_simp_lemmas     : tactic simp_lemmas
 /- (simp_lemmas_insert_core m lemmas id lemma priority) adds the given lemma to the set simp_lemmas. -/
 meta_constant simp_lemmas_insert_core : transparency → simp_lemmas → expr → tactic simp_lemmas