diff --git a/src/Lean/Meta/Tactic/Rewrites.lean b/src/Lean/Meta/Tactic/Rewrites.lean
index 7167412b94..68b873533d 100644
--- a/src/Lean/Meta/Tactic/Rewrites.lean
+++ b/src/Lean/Meta/Tactic/Rewrites.lean
@@ -7,7 +7,7 @@ prelude
 import Lean.Meta.LazyDiscrTree
 import Lean.Meta.Tactic.Assumption
 import Lean.Meta.Tactic.Rewrite
-import Lean.Meta.Tactic.Rfl
+import Lean.Meta.Tactic.Refl
 import Lean.Meta.Tactic.SolveByElim
 import Lean.Meta.Tactic.TryThis
 import Lean.Util.Heartbeats
@@ -149,7 +149,7 @@ def dischargableWithRfl? (mctx : MetavarContext) (e : Expr) : MetaM Bool := do
   try
     withoutModifyingState <| withMCtx mctx do
       -- We use `withReducible` here to follow the behaviour of `rw`.
-      withReducible (← mkFreshExprMVar e).mvarId!.applyRfl
+      withReducible (← mkFreshExprMVar e).mvarId!.refl
       pure true
   catch _e =>
     pure false