diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index 18bcf9013..e20d2cf3c 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -263,9 +263,14 @@ struct inductive_cmd_fn {
                 m_p.check_token_next(get_rparen_tk(), "invalid introduction rule, ')' expected");
                 m_implicit_infer_map.insert(intro_name, implicit_infer_kind::None);
             }
-            m_p.check_token_next(get_colon_tk(), "invalid introduction rule, ':' expected");
-            expr intro_type = m_p.parse_expr();
-            intros.push_back(intro_rule(intro_name, intro_type));
+            if (!m_params.empty() || m_p.curr_is_token(get_colon_tk())) {
+                m_p.check_token_next(get_colon_tk(), "invalid introduction rule, ':' expected");
+                expr intro_type = m_p.parse_expr();
+                intros.push_back(intro_rule(intro_name, intro_type));
+            } else {
+                expr intro_type = mk_constant(ind_name);
+                intros.push_back(intro_rule(intro_name, intro_type));
+            }
             if (!m_p.curr_is_token(get_comma_tk()))
                 break;
             m_p.next();
diff --git a/tests/lean/run/enum.lean b/tests/lean/run/enum.lean
new file mode 100644
index 000000000..8a7f3e558
--- /dev/null
+++ b/tests/lean/run/enum.lean
@@ -0,0 +1,16 @@
+import logic
+
+inductive Three :=
+zero : Three,
+one  : Three,
+two  : Three
+
+namespace Three
+
+  theorem disj (a : Three) : a = zero ∨ a = one ∨ a = two :=
+  rec (or.inl rfl) (or.inr (or.inl rfl)) (or.inr (or.inr rfl)) a
+
+  theorem example (a : Three) : a ≠ zero → a ≠ one → a = two :=
+  rec (λ h₁ h₂, absurd rfl h₁) (λ h₁ h₂, absurd rfl h₂) (λ h₁ h₂, rfl) a
+
+end Three