diff --git a/SSA/Projects/Scf/ScfFunctor.lean b/SSA/Projects/Scf/ScfFunctor.lean
index 75ebfb15f..e82fd4026 100644
--- a/SSA/Projects/Scf/ScfFunctor.lean
+++ b/SSA/Projects/Scf/ScfFunctor.lean
@@ -537,7 +537,7 @@ open ScfRegion in
 theorem correct :
     Com.denote (lhs rgn niters1 niters2 start1) Γv = Com.denote (rhs rgn niters1 niters2 start1) Γv := by
   simp [lhs, rhs, for_, axpy, cst]
-  try simp_peephole [add, iterate, for_, axpy, cst, cst_nat] at Γv
+  simp_peephole [add, iterate, for_, axpy, cst, cst_nat] at Γv
   intros a
   have swap_niters := add_comm (a := niters1) (b := niters2)
   set arg := ((LoopBody.CounterDecorator 1 fun i v =>