diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index aed8f474c1..0bb78ed0e6 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1378,7 +1378,8 @@ void elaborator::invoke_tactics(checkpoint const & C) {
     if (to_process.empty()) return;
     unassigned_uvars_to_params();
 
-    scope_elaborate_fn scope(nested_elaborate);
+    elaborate_fn fn(nested_elaborate);
+    scope_elaborate_fn scope(fn);
 
     unsigned i = to_process.size();
     while (i > 0) {
diff --git a/src/frontends/lean/old_elaborator.cpp b/src/frontends/lean/old_elaborator.cpp
index adb85848b7..638ef0d936 100644
--- a/src/frontends/lean/old_elaborator.cpp
+++ b/src/frontends/lean/old_elaborator.cpp
@@ -1683,7 +1683,8 @@ static tactic_state to_tactic_state(environment const & env, options const & opt
 }
 
 optional<tactic_state> old_elaborator::execute_tactic(expr const & tactic, tactic_state const & s, expr const & mvar) {
-    scope_elaborate_fn scope(nested_elaborate);
+    elaborate_fn fn(nested_elaborate);
+    scope_elaborate_fn scope(fn);
 
     name tactic_name("_tactic");
     expr tactic_type = ::lean::mk_app(mk_constant("tactic", {mk_level_one()}), mk_constant("unit"));