diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean
index ff90da6f54..187f6ccc87 100644
--- a/library/init/meta/smt/interactive.lean
+++ b/library/init/meta/smt/interactive.lean
@@ -229,7 +229,7 @@ open tactic
 
 /-- Simplify the target type of the main goal. -/
 meta def simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simp_config := {}) : smt_tactic unit :=
-tactic.interactive.simp hs attr_names ids [] cfg
+tactic.interactive.simp hs attr_names ids (loc.ns []) cfg
 
 /-- Simplify the target type of the main goal using simplification lemmas and the current set of hypotheses. -/
 meta def simp_using_hs (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simp_config := {}) : smt_tactic unit :=
@@ -239,7 +239,7 @@ meta def simph (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list)
 simp_using_hs hs attr_names ids cfg
 
 meta def dsimp (es : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : smt_tactic unit :=
-tactic.interactive.dsimp es attr_names ids []
+tactic.interactive.dsimp es attr_names ids (loc.ns [])
 
 meta def rsimp : smt_tactic unit :=
 do ccs ← to_cc_state, _root_.rsimp.rsimplify_goal ccs