diff --git a/SSA/Core/Tactic.lean b/SSA/Core/Tactic.lean
index 842fc5847..6b0854daf 100644
--- a/SSA/Core/Tactic.lean
+++ b/SSA/Core/Tactic.lean
@@ -57,7 +57,7 @@ macro "simp_peephole" "[" ts: Lean.Parser.Tactic.simpLemma,* "]" "at" ll:ident :
   `(tactic|
       (
       change_mlir_context $ll
-      simp (config := {failIfUnchanged := false, decide := false, unfoldPartialApp := true, zetaDelta := true}) only [
+      simp (config := {failIfUnchanged := false, decide := false }) only [
         Int.ofNat_eq_coe, Nat.cast_zero, DerivedCtxt.snoc, DerivedCtxt.ofCtxt,
         DerivedCtxt.ofCtxt_empty, Valuation.snoc_last,
         Com.denote, Expr.denote, HVector.denote, Var.zero_eq_last, Var.succ_eq_toSnoc,
diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean
index 0fed64420..7edb1fa59 100644
--- a/SSA/Projects/InstCombine/Tactic.lean
+++ b/SSA/Projects/InstCombine/Tactic.lean
@@ -27,7 +27,7 @@ macro "simp_alive_peephole" : tactic =>
         dsimp only [Com.Refinement]
         intros Γv
         simp_peephole [InstCombine.Op.denote] at Γv
-        simp (config := {failIfUnchanged := false, unfoldPartialApp := true, zetaDelta := true}) only [
+        simp (config := {failIfUnchanged := false}) only [
             BitVec.Refinement, bind, Option.bind, pure,
             simp_llvm,
             BitVec.bitvec_minus_one