diff --git a/src/Lean/Meta/Tactic/Cbv/Main.lean b/src/Lean/Meta/Tactic/Cbv/Main.lean
index ad1117e04c..fedec47fde 100644
--- a/src/Lean/Meta/Tactic/Cbv/Main.lean
+++ b/src/Lean/Meta/Tactic/Cbv/Main.lean
@@ -24,10 +24,6 @@ public register_builtin_option cbv.warning : Bool := {
   descr    := "disable `cbv` usage warning"
 }
 
-def tryMatchEquations (appFn : Name) : Simproc := fun e => do
-  let thms ← getMatchTheorems appFn
-  thms.rewrite (d := dischargeNone) e
-
 def tryEquations : Simproc := fun e => do
   unless e.isApp do
     return .rfl
@@ -42,18 +38,6 @@ def tryUnfold : Simproc := fun e => do
   let some thm ← getUnfoldTheorem appFn | return .rfl
   Theorem.rewrite thm e
 
-def tryMatcher : Simproc := fun e => do
-  unless e.isApp do
-    return .rfl
-  let some appFn := e.getAppFn.constName? | return .rfl
-  let some info ← getMatcherInfo? appFn | return .rfl
-  let start := info.numParams + 1
-  let stop  := start + info.numDiscrs
-  (simpAppArgRange · start stop)
-    >> tryMatchEquations appFn
-      <|> reduceRecMatcher
-        <| e
-
 def handleConstApp : Simproc := fun e => do
   if (← isCbvOpaque e.getAppFn.constName!) then
     return .rfl (done := true)