diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Nat.thy	Tue May 23 21:43:36 2023 +0200
@@ -1968,19 +1968,19 @@
 
 simproc_setup nateq_cancel_sums
   ("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") =
-  \<open>fn phi => try o Nat_Arith.cancel_eq_conv\<close>
+  \<open>K (try o Nat_Arith.cancel_eq_conv)\<close>
 
 simproc_setup natless_cancel_sums
   ("(l::nat) + m < n" | "(l::nat) < m + n" | "Suc m < n" | "m < Suc n") =
-  \<open>fn phi => try o Nat_Arith.cancel_less_conv\<close>
+  \<open>K (try o Nat_Arith.cancel_less_conv)\<close>
 
 simproc_setup natle_cancel_sums
   ("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" | "Suc m \<le> n" | "m \<le> Suc n") =
-  \<open>fn phi => try o Nat_Arith.cancel_le_conv\<close>
+  \<open>K (try o Nat_Arith.cancel_le_conv)\<close>
 
 simproc_setup natdiff_cancel_sums
   ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
-  \<open>fn phi => try o Nat_Arith.cancel_diff_conv\<close>
+  \<open>K (try o Nat_Arith.cancel_diff_conv)\<close>
 
 context order
 begin