diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean
index 890d48fc92..c670f07203 100644
--- a/src/Init/Lean/Elab/Command.lean
+++ b/src/Init/Lean/Elab/Command.lean
@@ -533,7 +533,7 @@ let resetMessages : CommandElabM MessageLog := do {
   pure messages
 };
 let restoreMessages (prevMessages : MessageLog) : CommandElabM Unit := do {
-  modify $ fun s => { messages := prevMessages ++ s.messages.eraseErrors, .. s }
+  modify $ fun s => { messages := prevMessages ++ s.messages.errorsToWarnings, .. s }
 };
 prevMessages ← resetMessages;
 succeeded ← finally (catch (do x; hasNoErrorMessages) (fun ex => pure false)) (restoreMessages prevMessages);
diff --git a/src/Init/Lean/Message.lean b/src/Init/Lean/Message.lean
index b245ea1d32..5ee4707a15 100644
--- a/src/Init/Lean/Message.lean
+++ b/src/Init/Lean/Message.lean
@@ -166,8 +166,8 @@ log.msgs.any $ fun m => match m.severity with
 | MessageSeverity.error => true
 | _                     => false
 
-def eraseErrors (log : MessageLog) : MessageLog :=
-{ msgs := log.msgs.foldl (fun r m => match m.severity with | MessageSeverity.error => r | _ => r.push m) {} }
+def errorsToWarnings (log : MessageLog) : MessageLog :=
+{ msgs := log.msgs.map (fun m => match m.severity with | MessageSeverity.error => { severity := MessageSeverity.warning, .. m} | _ => m) }
 
 def forM {m : Type → Type} [Monad m] (log : MessageLog) (f : Message → m Unit) : m Unit :=
 log.msgs.forM f