diff --git a/src/Lean/Elab/Tactic/Classical.lean b/src/Lean/Elab/Tactic/Classical.lean
index 2d3e54126f..6abca3eecc 100644
--- a/src/Lean/Elab/Tactic/Classical.lean
+++ b/src/Lean/Elab/Tactic/Classical.lean
@@ -30,6 +30,7 @@ def classical [Monad m] [MonadEnv m] [MonadFinally m] [MonadLiftT MetaM m] (t :
 
 @[builtin_tactic Lean.Parser.Tactic.classical, builtin_incremental]
 def evalClassical : Tactic := fun stx =>
-  classical <| Term.withNarrowedArgTacticReuse (argIdx := 1) Elab.Tactic.evalTactic stx
+  classical <| withSaveInfoContext <|
+    Term.withNarrowedArgTacticReuse (argIdx := 1) Elab.Tactic.evalTactic stx
 
 end Lean.Elab.Tactic