diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 2aed1dfb6a..5ef71672f2 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -23,7 +23,7 @@ private def resumeElabTerm (stx : Syntax) (expectedType? : Option Expr) (errToSo
   It is used to implement `synthesizeSyntheticMVars`. -/
 private def resumePostponed (savedContext : SavedContext) (stx : Syntax) (mvarId : MVarId) (postponeOnError : Bool) : TermElabM Bool :=
   withRef stx <| withMVarContext mvarId do
-    let s ← get
+    let s ← saveState
     try
       withSavedContext savedContext do
         let mvarDecl     ← getMVarDecl mvarId
@@ -42,13 +42,13 @@ private def resumePostponed (savedContext : SavedContext) (stx : Syntax) (mvarId
     catch
      | ex@(.internal id _) =>
        if id == postponeExceptionId then
-         set s
+         s.restore (restoreInfo := true)
          return false
        else
          throw ex
      | ex@(.error ..) =>
        if postponeOnError then
-         set s
+         s.restore (restoreInfo := true)
          return false
        else
          logException ex
diff --git a/tests/lean/run/1200.lean b/tests/lean/run/1200.lean
index ab113ce2bd..e04343c048 100644
--- a/tests/lean/run/1200.lean
+++ b/tests/lean/run/1200.lean
@@ -1,5 +1,5 @@
 example
-(h: match .none (α:=α) with
+(h: match none (α:=α) with
 | some _ => True
 | _      => True):
   True := by