revert change

leanprover · Nov 22, 2023 · 1e11c50 · 1e11c50
1 parent 0831ae8
commit 1e11c50
Showing 1 changed file with 2 additions and 8 deletions.
diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
@@ -45,15 +45,9 @@ structure State where
 
 abbrev SimpM := ReaderT Context $ StateRefT State MetaM
 
-structure SavedState where
-  meta : Meta.SavedState
-  usedTheorems : UsedSimps
-
 instance : MonadBacktrack SavedState SimpM where
-  saveState      := return ⟨← Meta.saveState, (← get).usedTheorems⟩
-  restoreState s := do
-    s.meta.restore
-    modify fun t => { t with usedTheorems := s.usedTheorems }
+  saveState      := Meta.saveState
+  restoreState s := s.restore
 
 inductive Step where
   | visit : Result → Step