From ec4794ad103ddfdbc3669587c19bb09f8b9c700b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 6 Jul 2022 13:55:57 -0700
Subject: [PATCH] chore: use `withAssignableSyntheticOpaque`

---
 src/Lean/Elab/Tactic/ElabTerm.lean  | 2 +-
 src/Lean/Elab/Tactic/Induction.lean | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index c19ebbc9fe..730792c876 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -38,7 +38,7 @@ def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (mayPostpo
     let eType ← inferType e
     -- We allow synthetic opaque metavars to be assigned in the following step since the `isDefEq` is not really
     -- part of the elaboration, but part of the tactic. See issue #492
-    unless (← withAssignableSyntheticOpaque do isDefEq eType expectedType) do
+    unless (← withAssignableSyntheticOpaque <| isDefEq eType expectedType) do
       Term.throwTypeMismatchError none expectedType eType e
     return e
 
diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index b8a46f7076..723912572c 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -127,7 +127,7 @@ partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name)
           throwError "insufficient number of targets for '{elimInfo.name}'"
         let target := ctx.targets[s.targetPos]!
         let expectedType ← getArgExpectedType
-        let target ← withConfig (fun cfg => { cfg with assignSyntheticOpaque := true }) do Term.ensureHasType expectedType target
+        let target ← withAssignableSyntheticOpaque <| Term.ensureHasType expectedType target
         modify fun s => { s with targetPos := s.targetPos + 1 }
         addNewArg target
       else match c.binderInfo with