diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index 4a6c8a5d6e..c5643ce867 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -590,7 +590,7 @@ modify $ fun s => { syntheticMVars := [], .. s };
 -- We use `filterRevM` instead of `filterM` to make sure we process the synthetic metavariables using the order they were created.
 -- It would not be incorrect to use `filterM`.
 remainingSyntheticMVars ← syntheticMVars.filterRevM $ fun mvarDecl => do {
-   trace `Elab.postpone mvarDecl.ref $ fun _ => fmt "resuming";
+   trace `Elab.postpone mvarDecl.ref $ fun _ => "resuming ?" ++ mvarDecl.mvarId;
    succeeded ← synthesizeSyntheticMVar mvarDecl;
    trace `Elab.postpone mvarDecl.ref $ fun _ => if succeeded then fmt "succeeded" else fmt "not ready yet";
    pure $ !succeeded