diff --git a/src/Lean/Meta/Tactic/Refl.lean b/src/Lean/Meta/Tactic/Refl.lean
index 15ed85289f..5f70029573 100644
--- a/src/Lean/Meta/Tactic/Refl.lean
+++ b/src/Lean/Meta/Tactic/Refl.lean
@@ -10,12 +10,6 @@ import Lean.Meta.Tactic.Apply
 
 namespace Lean.Meta
 
-private def useKernel (lhs rhs : Expr) : MetaM Bool := do
-  if lhs.hasFVar || lhs.hasMVar || rhs.hasFVar || rhs.hasMVar then
-    return false
-  else
-    return (← getTransparency) matches TransparencyMode.default | TransparencyMode.all
-
 /--
 Close given goal using `Eq.refl`.
 -/
@@ -27,10 +21,7 @@ def _root_.Lean.MVarId.refl (mvarId : MVarId) : MetaM Unit := do
       throwTacticEx `rfl mvarId m!"equality expected{indentExpr targetType}"
     let lhs ← instantiateMVars targetType.appFn!.appArg!
     let rhs ← instantiateMVars targetType.appArg!
-    let success ← if (← useKernel lhs rhs) then
-      ofExceptKernelException (Kernel.isDefEq (← getEnv) {} lhs rhs)
-    else
-      isDefEq lhs rhs
+    let success ← isDefEq lhs rhs
     unless success do
       throwTacticEx `rfl mvarId m!"equality lhs{indentExpr lhs}\nis not definitionally equal to rhs{indentExpr rhs}"
     let us := targetType.getAppFn.constLevels!
diff --git a/tests/lean/run/4644.lean b/tests/lean/run/4644.lean
index fd1dc490db..c4c5612a4c 100644
--- a/tests/lean/run/4644.lean
+++ b/tests/lean/run/4644.lean
@@ -10,9 +10,17 @@ termination_by a.size - i
 def check_sorted [x: LE α] [DecidableRel x.le] (a: Array α): Bool :=
   sorted_from_var a 0
 
--- works (because `rfl` of closed terms resorts to kernel defeq, see #3772)
-example: check_sorted #[0, 3, 3, 5, 8, 10, 10, 10] := by
-  rfl
+/--
+error: The rfl tactic failed. Possible reasons:
+- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
+- The arguments of the relation are not equal.
+Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
+`exact HEq.rfl` etc.
+⊢ check_sorted #[0, 3, 3, 5, 8, 10, 10, 10] = true
+-/
+#guard_msgs in
+example: check_sorted #[0, 3, 3, 5, 8, 10, 10, 10] = true := by
+  rfl -- fails because `rfl` uses `.default` transparency, and `sorted_from_var` is marked as irreducible
 
 /--
 error: tactic 'decide' failed for proposition
diff --git a/tests/lean/run/ack.lean b/tests/lean/run/ack.lean
index ed2f68c22b..974c4d1e28 100644
--- a/tests/lean/run/ack.lean
+++ b/tests/lean/run/ack.lean
@@ -25,17 +25,3 @@ set_option diagnostics.threshold 500 in
 set_option diagnostics true in
 theorem ex : ack 3 2 = 29 :=
   rfl
-
-
-/--
-info: [kernel] unfolded declarations (max: 1193, num: 4):
-  [kernel] Nat.casesOn ↦ 1193
-  [kernel] Nat.rec ↦ 1065
-  [kernel] Eq.ndrec ↦ 973
-  [kernel] Eq.rec ↦ 973use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
--/
-#guard_msgs in
-set_option diagnostics true in
-set_option diagnostics.threshold 800 in
-theorem ack_3_2_eq_29 : ack 3 2 = 29 := by
-  rfl -- uses kernel defeq checker, so only kernel diags shown
diff --git a/tests/lean/run/treeNode.lean b/tests/lean/run/treeNode.lean
index 77c9bb0090..40f7a318fc 100644
--- a/tests/lean/run/treeNode.lean
+++ b/tests/lean/run/treeNode.lean
@@ -37,5 +37,5 @@ theorem length_treeToList_eq_numNames (t : TreeNode) : (treeToList t).length = n
 where
   helper (cs : List TreeNode) : (cs.map treeToList).join.length = numNamesLst cs := by
     match cs with
-    | [] => rfl
+    | [] => simp [List.join, numNamesLst]
     | c::cs' => simp [List.join, List.map, numNamesLst, length_treeToList_eq_numNames c, helper cs']
diff --git a/tests/lean/run/wfirred.lean b/tests/lean/run/wfirred.lean
index ee96ba698a..89fbfcbc9f 100644
--- a/tests/lean/run/wfirred.lean
+++ b/tests/lean/run/wfirred.lean
@@ -29,7 +29,15 @@ but is expected to have type
 #guard_msgs in
 example : foo (n+1) = foo n := rfl
 
--- This succeeding is a bug or misfeature in the rfl tactic, using the kernel defeq check
+-- also for closed terms
+/--
+error: The rfl tactic failed. Possible reasons:
+- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
+- The arguments of the relation are not equal.
+Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
+`exact HEq.rfl` etc.
+⊢ foo 0 = 0
+-/
 #guard_msgs in
 example : foo 0 = 0 := by rfl