diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 19e4bbddcc..2af540ea84 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -305,7 +305,7 @@ def withoutModifyingElabMetaStateWithInfo (x : TermElabM α) : TermElabM α := d
 private def withoutModifyingStateWithInfoAndMessagesImpl (x : TermElabM α) : TermElabM α := do
   let saved ← saveState
   try
-    x
+    withSaveInfoContext x
   finally
     let s ← get
     let saved := { saved with elab.infoState := s.infoState, elab.messages := s.messages }