From 618b22e9a19adb84639035f9be3a0508af5474ee Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 3 Dec 2019 12:53:37 -0800
Subject: [PATCH] fix: typo

---
 src/Init/Lean/Meta/SynthInstance.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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