diff --git a/src/Init/Lean/Meta/SynthInstance.lean b/src/Init/Lean/Meta/SynthInstance.lean
index 2e18f80c4e..00b13e47fb 100644
--- a/src/Init/Lean/Meta/SynthInstance.lean
+++ b/src/Init/Lean/Meta/SynthInstance.lean
@@ -289,7 +289,7 @@ match cNode.subgoals with
   newAnswer cNode.key answer
 | mvar::_ => do
    let waiter := Waiter.consumerNode cNode;
-   let key := mkTableKey cNode.mctx mvar;
+   key ← mkTableKeyFor cNode.mctx mvar;
    entry? ← findEntry key;
    match entry? with
    | none       => newSubgoal cNode.mctx key mvar waiter