diff --git a/src/Lean/Meta/Tactic/Replace.lean b/src/Lean/Meta/Tactic/Replace.lean
index 8a7999b2b8..ed953a874e 100644
--- a/src/Lean/Meta/Tactic/Replace.lean
+++ b/src/Lean/Meta/Tactic/Replace.lean
@@ -25,8 +25,8 @@ withMVarContext mvarId do
   u        ← getLevel target;
   eq       ← mkEq target targetNew;
   newProof ← mkExpectedTypeHint eqProof eq;
-  let newVal := mkAppN (Lean.mkConst `Eq.mpr [u]) #[target, targetNew, eqProof, mvarNew];
-  assignExprMVar mvarId mvarNew;
+  let val  := mkAppN (Lean.mkConst `Eq.mpr [u]) #[target, targetNew, eqProof, mvarNew];
+  assignExprMVar mvarId val;
   pure mvarNew.mvarId!
 
 /--