diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index 3e080400a..d7927c404 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -379,7 +379,7 @@ struct inductive_cmd_fn {
                                  [&](inductive_decl const & d) { return const_name(e) == inductive_decl_name(d); }))
                     return none_expr();
                 // found target
-                expr r = mk_app(mk_explicit(e), section_params);
+                expr r = mk_implicit(mk_app(mk_explicit(e), section_params));
                 return some_expr(r);
             });
     }
@@ -512,15 +512,16 @@ struct inductive_cmd_fn {
     }
 
     /** \brief Create an alias for the fully qualified name \c full_id. */
-    environment create_alias(environment env, bool composite, name const & full_id, levels const & section_leves, buffer<expr> const & section_params) {
+    environment create_alias(environment env, bool composite, name const & full_id, levels const & section_levels, buffer<expr> const & section_params) {
         name id;
         if (composite)
             id = name(name(full_id.get_prefix().get_string()), full_id.get_string());
         else
             id = name(full_id.get_string());
         if (in_section_or_context(env)) {
-            expr r = mk_explicit(mk_constant(full_id, section_leves));
+            expr r = mk_explicit(mk_constant(full_id, section_levels));
             r = mk_app(r, section_params);
+            r = mk_implicit(r);
             m_p.add_local_expr(id, r);
         }
         if (full_id != id)
diff --git a/tests/lean/run/class_bug1.lean b/tests/lean/run/class_bug1.lean
new file mode 100644
index 000000000..ed04648da
--- /dev/null
+++ b/tests/lean/run/class_bug1.lean
@@ -0,0 +1,27 @@
+import logic
+
+inductive category (ob : Type) (mor : ob → ob → Type) : Type :=
+mk : Π (comp : Π⦃A B C : ob⦄, mor B C → mor A B → mor A C)
+           (id : Π {A : ob}, mor A A),
+            (Π {A B C D : ob} {f : mor A B} {g : mor B C} {h : mor C D},
+            comp h (comp g f) = comp (comp h g) f) →
+           (Π {A B : ob} {f : mor A B}, comp f id = f) →
+           (Π {A B : ob} {f : mor A B}, comp id f = f) →
+            category ob mor
+class category
+
+namespace category
+section sec_cat
+  parameter A : Type
+  inductive foo :=
+  mk : A → foo
+
+  class foo
+  parameters {ob : Type} {mor : ob → ob → Type} {Cat : category ob mor}
+  abbreviation compose := rec (λ comp id assoc idr idl, comp) Cat
+  abbreviation id := rec (λ comp id assoc idr idl, id) Cat
+  infixr `∘`:60 := compose
+  inductive is_section {A B : ob} (f : mor A B) : Type :=
+  mk : ∀g, g ∘ f = id → is_section f
+end sec_cat
+end category