diff --git a/src/Lean/Meta/Constructions.lean b/src/Lean/Meta/Constructions.lean
index 5865d4b0b2..ee9ecfcdb7 100644
--- a/src/Lean/Meta/Constructions.lean
+++ b/src/Lean/Meta/Constructions.lean
@@ -114,6 +114,7 @@ where
         hints       := ReducibilityHints.abbrev
       }
       setReducibleAttribute declName
+      modifyEnv fun env => markNoConfusion env declName
 
 def mkNoConfusion (declName : Name) : MetaM Unit := do
   if (← isEnumType declName) then
diff --git a/tests/lean/run/enumNoConfusionIssue.lean b/tests/lean/run/enumNoConfusionIssue.lean
new file mode 100644
index 0000000000..5324dd263c
--- /dev/null
+++ b/tests/lean/run/enumNoConfusionIssue.lean
@@ -0,0 +1,13 @@
+inductive MyBool :=
+  | MyTrue
+  | MyFalse
+
+inductive T :=
+  | mk (b: MyBool) (u: Unit)
+
+inductive isTrue: T → Type :=
+  | intro: isTrue (.mk .MyTrue ())
+
+example {τ: T} (h: isTrue τ): Unit :=
+  match τ, h with
+  | .mk .MyTrue (), .intro => ()