diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean
index f6c2c69253..770228608a 100644
--- a/library/init/meta/simp_tactic.lean
+++ b/library/init/meta/simp_tactic.lean
@@ -410,9 +410,12 @@ meta def join_user_simp_lemmas_core : simp_lemmas → list name → tactic simp_
 | S []             := return S
 | S (attr_name::R) := do S' ← get_user_simp_lemmas attr_name, join_user_simp_lemmas_core (S.join S') R
 
-meta def join_user_simp_lemmas (no_dflt : bool) : list name → tactic simp_lemmas
-| []         := if no_dflt then pure simp_lemmas.mk else simp_lemmas.mk_default
-| attr_names := join_user_simp_lemmas_core simp_lemmas.mk attr_names
+meta def join_user_simp_lemmas (no_dflt : bool) (attrs : list name) : tactic simp_lemmas :=
+if no_dflt then
+  join_user_simp_lemmas_core simp_lemmas.mk attrs
+else do
+  s ← simp_lemmas.mk_default,
+  join_user_simp_lemmas_core s attrs
 
 /- Normalize numerical expression, returns a pair (n, pr) where n is the resultant numeral,
    and pr is a proof that the input argument is equal to n. -/