diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean
index b6535d4bc8..64cee71ee4 100644
--- a/library/init/meta/smt/interactive.lean
+++ b/library/init/meta/smt/interactive.lean
@@ -22,7 +22,7 @@ meta def step {α : Type} (tac : smt_tactic α) : smt_tactic unit :=
 tac >> solve_goals
 
 meta def istep {α : Type} (line0 col0 line col : nat) (tac : smt_tactic α) : smt_tactic unit :=
-λ ss ts, (@scope_trace _ line col ((tac >> solve_goals) ss ts)).clamp_pos line0 line col
+λ ss ts, (@scope_trace _ line col (λ _, (tac >> solve_goals) ss ts)).clamp_pos line0 line col
 
 meta def execute (tac : smt_tactic unit) : tactic unit :=
 using_smt tac
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 629975c894..fd77a70238 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -477,7 +477,7 @@ meta def step {α : Type u} (t : tactic α) : tactic unit :=
 t >>[tactic] cleanup
 
 meta def istep {α : Type u} (line0 col0 : ℕ) (line col : ℕ) (t : tactic α) : tactic unit :=
-λ s, (@scope_trace _ line col (step t s)).clamp_pos line0 line col
+λ s, (@scope_trace _ line col (λ _, step t s)).clamp_pos line0 line col
 
 meta def is_prop (e : expr) : tactic bool :=
 do t ← infer_type e,