diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index ee17c630f8..9c59372351 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -300,7 +300,7 @@ static environment variable_cmd_core(parser & p, variable_kind k, bool is_protec
     }
     level_param_names new_ls;
     list<expr> ctx = p.locals_to_context();
-    std::tie(type, new_ls) = p.old_elaborate_type(type, ctx);
+    std::tie(type, new_ls) = p.elaborate_type(ctx, type);
     if (k == variable_kind::Variable || k == variable_kind::Parameter)
         update_local_levels(p, new_ls, k == variable_kind::Variable);
     return declare_var(p, p.env(), n, append(ls, new_ls), type, k, bi, pos, is_protected);
diff --git a/tests/lean/858.lean.expected.out b/tests/lean/858.lean.expected.out
index 574ab706ab..784c6ef931 100644
--- a/tests/lean/858.lean.expected.out
+++ b/tests/lean/858.lean.expected.out
@@ -1,2 +1,3 @@
-858.lean:2:2: error: failed to add declaration 'n' to local context, type has metavariables
-  ?M_1 → ℕ
+858.lean:2:18: error: don't know how to synthesize placeholder
+state:
+⊢ Type
diff --git a/tests/lean/const.lean b/tests/lean/const.lean
index 6548a3dbc8..2e4bba4254 100644
--- a/tests/lean/const.lean
+++ b/tests/lean/const.lean
@@ -11,7 +11,7 @@ set_option pp.implicit true
 section
   variable A : Type
   variable S : inhabited A
-  variable B : @bla A _
+  variable B : @bla A S
   check B
   check @foo A S
 end