From 294b1d5839ac2b61b237d3e258f773dbd1bdf2eb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 19 Jun 2024 01:39:16 +0200
Subject: [PATCH] chore: cleanup (#4494)

closes #4287
closes #4288
---
 src/Init/Prelude.lean            | 2 +-
 src/Lean/Meta/SynthInstance.lean | 3 ---
 2 files changed, 1 insertion(+), 4 deletions(-)

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index faab0d139e..43be55f701 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -2976,7 +2976,7 @@ def MonadExcept.ofExcept [Monad m] [MonadExcept ε m] : Except ε α → m α
 
 export MonadExcept (throw tryCatch ofExcept)
 
-instance (ε : outParam (Type u)) (m : Type v → Type w) [MonadExceptOf ε m] : MonadExcept ε m where
+instance (ε : Type u) (m : Type v → Type w) [MonadExceptOf ε m] : MonadExcept ε m where
   throw    := throwThe ε
   tryCatch := tryCatchThe ε
 
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index bae085dae9..629578ce5f 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -194,9 +194,6 @@ def checkSystem : SynthM Unit := do
   Core.checkInterrupted
   Core.checkMaxHeartbeatsCore "typeclass" `synthInstance.maxHeartbeats (← read).maxHeartbeats
 
-@[inline] def mapMetaM (f : forall {α}, MetaM α → MetaM α) {α} : SynthM α → SynthM α :=
-  monadMap @f
-
 instance : Inhabited (SynthM α) where
   default := fun _ _ => default