diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean
index be65fe1d62..016d51da55 100644
--- a/src/Lean/Meta/DiscrTree.lean
+++ b/src/Lean/Meta/DiscrTree.lean
@@ -259,7 +259,7 @@ where
   step (e : Expr) := do
     let e ← whnfCore e
     match (← unfoldDefinition? e) with
-    | some e' => if isBadKey e' then return e else step e'
+    | some e' => if isBadKey e'.getAppFn then return e else step e'
     | none    => return e
 
 /-- whnf for the discrimination tree module -/
diff --git a/tests/lean/run/simpUnfoldAbbrev.lean b/tests/lean/run/simpUnfoldAbbrev.lean
new file mode 100644
index 0000000000..8379ac3f77
--- /dev/null
+++ b/tests/lean/run/simpUnfoldAbbrev.lean
@@ -0,0 +1,14 @@
+example {x y : Nat} (h : y > x) : x < y := by
+  -- simp should unfold `>` when inserting into the discrimination tree
+  simp [h]
+
+abbrev good (n : Nat) :=
+  n > 42
+
+example (h : good n) : n > 42 := by
+  -- simp should unfold `good` when inserting into the discrimination tree
+  simp [h]
+
+example {x y : Nat} (h : x ≠ y) : x ≠ y := by
+  -- ≠ is also an abbreviation
+  simp [h]