From 04eab3c70572bf82dc0c8feab37950eaaf171482 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 21 Aug 2020 13:08:49 -0700
Subject: [PATCH] chore: remove dead code

---
 src/Lean/Meta/Basic.lean     | 7 -------
 src/Lean/Meta/Exception.lean | 5 -----
 2 files changed, 12 deletions(-)

diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 724301d4fb..a32e57cd7d 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -287,13 +287,6 @@ mvarId ← mkFreshId;
 modify $ fun s => { s with mctx := s.mctx.addLevelMVarDecl mvarId };
 pure $ mkLevelMVar mvarId
 
-@[inline] def throwEx {α} (f : ExceptionContext → Exception) : MetaM α := do
-env  ← getEnv;
-mctx ← getMCtx;
-lctx ← getLCtx;
-opts ← getOptions;
-throw (f { env := env, mctx := mctx, lctx := lctx, opts := opts })
-
 @[inline] def ofExcept {α ε} [HasToString ε] (x : Except ε α) : MetaM α :=
 match x with
 | Except.ok a    => pure a
diff --git a/src/Lean/Meta/Exception.lean b/src/Lean/Meta/Exception.lean
index bd1f25201c..bb253c01b8 100644
--- a/src/Lean/Meta/Exception.lean
+++ b/src/Lean/Meta/Exception.lean
@@ -12,8 +12,6 @@ import Lean.Util.PPGoal
 namespace Lean
 namespace Meta
 
-abbrev ExceptionContext := MessageDataContext
-
 inductive Exception
 | isDefEqStuck
 | core          (ex : Core.Exception)
@@ -25,9 +23,6 @@ def getRef : Exception → Syntax
 | core ex => ex.ref
 | _       => Syntax.missing
 
-def mkCtx (ctx : ExceptionContext) (m : MessageData) : MessageData :=
-MessageData.withContext ctx m
-
 def toMessageData : Exception → MessageData
 | isDefEqStuck => "<isDefEqStuck>"
 | core ex      => ex.toMessageData