diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 8a08b89ffb..800dab3720 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -669,6 +669,8 @@ static expr replace_with_simple_metavars(metavar_context & mctx, expr const & e)
 
 static environment elab_cmd(parser & p) {
     expr e = p.parse_expr();
+    if (p.used_sorry())
+        p.declare_sorry();
     metavar_context mctx;
     expr new_e; level_param_names ls;
     std::tie(new_e, ls) = p.elaborate(mctx, e);
diff --git a/tests/lean/run/elab3.lean b/tests/lean/run/elab3.lean
new file mode 100644
index 0000000000..33e9bda54e
--- /dev/null
+++ b/tests/lean/run/elab3.lean
@@ -0,0 +1,3 @@
+set_option pp.binder_types true
+
+#elab (sorry : ∀ a, a > 0)