diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index d7927c404..095df7ece 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -259,7 +259,7 @@ struct inductive_cmd_fn {
     */
     void add_params_to_local_scope(expr d_type, buffer<expr> & params) {
         for (unsigned i = 0; i < m_num_params; i++) {
-            expr l = mk_local_for(d_type);
+            expr l = mk_local(m_p.mk_fresh_name(), binding_name(d_type), mk_as_is(binding_domain(d_type)), binding_info(d_type));
             m_p.add_local(l);
             params.push_back(l);
             d_type = instantiate(binding_body(d_type), l);
diff --git a/tests/lean/run/indbug2.lean b/tests/lean/run/indbug2.lean
new file mode 100644
index 000000000..468497c4f
--- /dev/null
+++ b/tests/lean/run/indbug2.lean
@@ -0,0 +1,6 @@
+section
+parameter {A : Type}
+definition foo : A → A → Type := (λ x y, Type)
+inductive bar {a b : A} (f : foo a b) :=
+bar2 : bar f
+end