diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
index 3247032039..16e08f370f 100644
--- a/src/Lean/Meta/Tactic/Simp/Types.lean
+++ b/src/Lean/Meta/Tactic/Simp/Types.lean
@@ -45,10 +45,6 @@ structure State where
 
 abbrev SimpM := ReaderT Context $ StateRefT State MetaM
 
-instance : MonadBacktrack SavedState SimpM where
-  saveState      := Meta.saveState
-  restoreState s := s.restore
-
 inductive Step where
   | visit : Result → Step
   | done  : Result → Step