diff --git a/src/Lean/Meta/Tactic/AC/Main.lean b/src/Lean/Meta/Tactic/AC/Main.lean
index 5c8cfc7b78..5de74ed8c9 100644
--- a/src/Lean/Meta/Tactic/AC/Main.lean
+++ b/src/Lean/Meta/Tactic/AC/Main.lean
@@ -171,7 +171,7 @@ where
 
 @[builtinTactic acRfl] def acRflTactic : Lean.Elab.Tactic.Tactic := fun _ => do
   let goal ← getMainGoal
-  rewriteUnnormalized goal
+  goal.withContext <| rewriteUnnormalized goal
 
 builtin_initialize
   registerTraceClass `Meta.AC
diff --git a/tests/lean/run/ac_rfl.lean b/tests/lean/run/ac_rfl.lean
index d7e2df4677..6e57a5e9cd 100644
--- a/tests/lean/run/ac_rfl.lean
+++ b/tests/lean/run/ac_rfl.lean
@@ -82,3 +82,6 @@ theorem ex₃ (n : Nat) : (fun x => n + x) = (fun x => x + n) := by
 -- Repro: the Prop universe doesn't work
 example (p q : Prop) : (p ∨ p ∨ q ∧ True) = (q ∨ p) := by
   ac_rfl
+
+-- Repro: missing withContext
+example : ∀ x : Nat, x = x := by intro x; ac_rfl