diff --git a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
index fbf95a280e..2d2ac8224e 100644
--- a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
@@ -102,6 +102,7 @@ def evalCheck (tacticName : Name) (k : GoalM Bool)
     let progress ← k
     unless progress do
       throwError "`{tacticName}` failed"
+    processNewFacts
     unless (← Grind.getConfig).verbose do
       return ()
     if (← get).inconsistent then