From 27c495c198768e63f630deff6476c0c680733c79 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 3 Nov 2020 15:09:10 -0800
Subject: [PATCH] fix: `Tactic.orelse` was using the wrong `try ... catch ...`

---
 src/Lean/Elab/Tactic/Basic.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index d929ccb87e..f99793b91e 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -51,15 +51,15 @@ def BacktrackableState.restore (b : BacktrackableState) : TacticM Unit := do
   let b ← saveBacktrackableState
   try x catch ex => b.restore; h ex
 
-@[inline] protected def orelse {α} (x y : TacticM α) : TacticM α := do
-  try x catch _ => y
-
 instance : MonadExcept Exception TacticM := {
   throw    := throw,
   tryCatch := Tactic.tryCatch
 }
 
-instance {α} : OrElse (TacticM α) := ⟨Tactic.orelse⟩
+@[inline] protected def orElse {α} (x y : TacticM α) : TacticM α := do
+  try x catch _ => y
+
+instance {α} : OrElse (TacticM α) := ⟨Tactic.orElse⟩
 
 structure SavedState :=
   (core   : Core.State)