diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index 03390e1786..c5ed7dc24f 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -421,6 +421,10 @@ mutual
     | _ => return none
 end
 
+def unfoldDefinition (e : Expr) : MetaM Expr := do
+  let some e ← unfoldDefinition? e | throwError! "failed to unfold definition{indentExpr e}"
+  return e
+
 @[specialize] partial def whnfHeadPred (e : Expr) (pred : Expr → MetaM Bool) : MetaM Expr :=
   whnfEasyCases e fun e => do
     let e ← whnfCore e