diff --git a/src/Lean/Compiler/LCNF/CompilerM.lean b/src/Lean/Compiler/LCNF/CompilerM.lean
index 534f65111b..2cb6887bbe 100644
--- a/src/Lean/Compiler/LCNF/CompilerM.lean
+++ b/src/Lean/Compiler/LCNF/CompilerM.lean
@@ -239,6 +239,10 @@ See `Check.lean` for the free variable substitution checker.
 @[inline, inheritDoc normExprImp] def normExpr [MonadFVarSubst m t] [Monad m] (e : Expr) : m Expr :=
   return normExprImp (← getSubst) e t
 
+@[inheritDoc normExprImp]
+abbrev normExprCore (s : FVarSubst) (e : Expr) (translator : Bool) : Expr :=
+  normExprImp s e translator
+
 /--
 Normalize the given expressions using the current substitution.
 -/