chore: remove dead code

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

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