From 966e1df96d1ddac05fc47f3439754673a3fbbeab Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 19 Nov 2022 07:43:54 -0800
Subject: [PATCH] chore: fix build

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

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 649fe3eb23..bfb8f9d92b 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -704,7 +704,7 @@ theorem decide_false_eq_false (h : Decidable False) : @decide False h = false :=
 
 /-- Similar to `decide`, but uses an explicit instance -/
 @[inline] def toBoolUsing {p : Prop} (d : Decidable p) : Bool :=
-  decide p (h := d)
+  decide (h := d)
 
 theorem toBoolUsing_eq_true {p : Prop} (d : Decidable p) (h : p) : toBoolUsing d = true :=
   decide_eq_true (inst := d) h