diff --git a/library/init/meta/smt/rsimp.lean b/library/init/meta/smt/rsimp.lean
index 6f7f67824a..baffb8ee1d 100644
--- a/library/init/meta/smt/rsimp.lean
+++ b/library/init/meta/smt/rsimp.lean
@@ -103,7 +103,7 @@ do t           ← target,
    try (replace_target new_t pr)
 
 meta def rsimplify_at (ccs : cc_state) (h : expr) (m : option repr_map := none) : tactic unit :=
-do tactic.when (expr.is_local_constant h = ff) (tactic.fail "tactic rsimplify_at failed, the given expression is not a hypothesis"),
+do when (expr.is_local_constant h = ff) (tactic.fail "tactic rsimplify_at failed, the given expression is not a hypothesis"),
    htype            ← infer_type h,
    (new_htype, heq) ← rsimplify ccs htype m,
    try $ do assert (expr.local_pp_name h) new_htype,
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 44b51fff7c..8ded8ff5df 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -716,10 +716,6 @@ do g::gs ← get_goals,
 meta instance : has_andthen (tactic unit) :=
 ⟨seq⟩
 
-/- Applies tac if c holds -/
-meta def when (c : Prop) [decidable c] (tac : tactic unit) : tactic unit :=
-if c then tac else skip
-
 meta constant is_trace_enabled_for : name → bool
 
 /- Execute tac only if option trace.n is set to true. -/