diff --git a/src/Lean/Meta/LevelDefEq.lean b/src/Lean/Meta/LevelDefEq.lean
index 3cbcca9e7d..1fbd04128c 100644
--- a/src/Lean/Meta/LevelDefEq.lean
+++ b/src/Lean/Meta/LevelDefEq.lean
@@ -213,6 +213,8 @@ private def restore (env : Environment) (mctx : MetavarContext) (postponed : Per
   try
     if (← x) then
       if (← processPostponed mayPostpone) then
+        let newPostponed ← getPostponed
+        setPostponed (postponed ++ newPostponed)
         return true
       else
         restore env mctx postponed