diff --git a/src/Lean/Util/MonadBacktrack.lean b/src/Lean/Util/MonadBacktrack.lean
index d0532d5a83..77b54c8d0f 100644
--- a/src/Lean/Util/MonadBacktrack.lean
+++ b/src/Lean/Util/MonadBacktrack.lean
@@ -37,6 +37,14 @@ export MonadBacktrack (saveState restoreState)
     restoreState s
     throw ex
 
+@[specialize] def commitIfNoEx [Monad m] [MonadBacktrack s m] [MonadExcept ε m] (x : m α) : m α := do
+  let s ← saveState
+  try
+    x
+  catch ex =>
+    restoreState s
+    throw ex
+
 @[specialize] def withoutModifyingState [Monad m] [MonadFinally m] [MonadBacktrack s m] (x : m α) : m α := do
   let s ← saveState
   try