diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index ac150cf623..0a9866cfb0 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -266,15 +266,16 @@ private def getOptRotation (stx : Syntax) : Nat :=
   for mvarId in mvarIds do
     unless (← mvarId.isAssigned) do
       setGoals [mvarId]
-      try
-        evalTactic stx[1]
-        mvarIdsNew := mvarIdsNew ++ (← getUnsolvedGoals)
-      catch ex =>
-        if (← read).recover then
-          logException ex
-          mvarIdsNew := mvarIdsNew.push mvarId
-        else
-          throw ex
+      mvarIdsNew ← Tactic.tryCatch
+        (do
+          evalTactic stx[1]
+          return mvarIdsNew ++ (← getUnsolvedGoals))
+        (fun ex => do
+          if (← read).recover then
+            logException ex
+            return mvarIdsNew.push mvarId
+          else
+            throw ex)
   setGoals mvarIdsNew.toList
 
 @[builtin_tactic Parser.Tactic.anyGoals] def evalAnyGoals : Tactic := fun stx => do
diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index eca414db66..6a3b0890c3 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/src/Lean/Elab/Tactic/Simp.lean
@@ -119,17 +119,22 @@ private def addDeclToUnfoldOrTheorem (thms : SimpTheorems) (id : Origin) (e : Ex
     thms.add id #[] e (post := post) (inv := inv)
 
 private def addSimpTheorem (thms : SimpTheorems) (id : Origin) (stx : Syntax) (post : Bool) (inv : Bool) : TermElabM SimpTheorems := do
-  let (levelParams, proof) ← Term.withoutModifyingElabMetaStateWithInfo <| withRef stx <| Term.withoutErrToSorry do
+  let thm? ← Term.withoutModifyingElabMetaStateWithInfo <| withRef stx do
     let e ← Term.elabTerm stx none
     Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
     let e ← instantiateMVars e
+    if e.hasSyntheticSorry then
+      return none
     let e := e.eta
     if e.hasMVar then
       let r ← abstractMVars e
-      return (r.paramNames, r.expr)
+      return some (r.paramNames, r.expr)
     else
-      return (#[], e)
-  thms.add id levelParams proof (post := post) (inv := inv)
+      return some (#[], e)
+  if let some (levelParams, proof) := thm? then
+    thms.add id levelParams proof (post := post) (inv := inv)
+  else
+    return thms
 
 structure ElabSimpArgsResult where
   ctx      : Simp.Context
@@ -167,7 +172,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
 
     syntax simpErase := "-" ident
     -/
-    withMainContext do
+    let go := withMainContext do
       let mut thmsArray := ctx.simpTheorems
       let mut thms      := thmsArray[0]!
       let mut simprocs  := simprocs
@@ -230,6 +235,12 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
           else
             throw ex
       return { ctx := { ctx with simpTheorems := thmsArray.set! 0 thms }, simprocs, starArg }
+    -- If recovery is disabled, then we want simp argument elaboration failures to be exceptions.
+    -- This affects `addSimpTheorem`.
+    if (← read).recover then
+      go
+    else
+      Term.withoutErrToSorry go
 where
   isSimproc? (e : Expr) : MetaM (Option Name) := do
     let .const declName _ := e | return none
diff --git a/tests/lean/run/4888.lean b/tests/lean/run/4888.lean
new file mode 100644
index 0000000000..c9d2a34ad3
--- /dev/null
+++ b/tests/lean/run/4888.lean
@@ -0,0 +1,20 @@
+/-!
+# `all_goals` should not consume error messages
+
+https://github.com/leanprover/lean4/issues/4888
+-/
+
+/--
+error: application type mismatch
+  Nat.succ True
+argument
+  True
+has type
+  Prop : Type
+but is expected to have type
+  Nat : Type
+-/
+#guard_msgs in
+theorem bug: True := by
+ all_goals exact Nat.succ True
+ trivial
diff --git a/tests/lean/run/simp-elab-recover.lean b/tests/lean/run/simp-elab-recover.lean
index 81428b19ba..a3539c3190 100644
--- a/tests/lean/run/simp-elab-recover.lean
+++ b/tests/lean/run/simp-elab-recover.lean
@@ -1,5 +1,5 @@
 /-!
-`simp [invaild]` makes progress which is great for interactive UX, but confusing
+`simp [invalid]` makes progress which is great for interactive UX, but confusing
 when inside a tactic combinator. This checks that without the `recover` flag,
 `simp [invalid]` fails.
 -/
@@ -25,3 +25,9 @@ example : 0 + n = n := by
 example : 0 + n = n := by
   skip <;> simp only [does_not_exist, Nat.zero_add]
   done
+
+/-- error: unknown identifier 'does_not_exist' -/
+#guard_msgs in
+example : 0 + n = n := by
+  all_goals simp only [does_not_exist, Nat.zero_add]
+  done