diff -r ac39d932ddfc -r b7d051e25d9d src/HOL/Tools/nat_arith.ML
--- a/src/HOL/Tools/nat_arith.ML	Sun Aug 18 15:29:03 2024 +0200
+++ b/src/HOL/Tools/nat_arith.ML	Sun Aug 18 15:29:18 2024 +0200
@@ -21,12 +21,12 @@
     [Conv.rewr_conv (Library.foldl (op RS) (@{thm nat_arith.rule0}, path)),
      Conv.arg_conv (Raw_Simplifier.rewrite ctxt false norm_rules)]
 
-fun add_atoms path (Const (\<^const_name>\<open>Groups.plus\<close>, _) $ x $ y) =
+fun add_atoms path \<^Const_>\<open>plus _ for x y\<close> =
       add_atoms (@{thm nat_arith.add1}::path) x #>
       add_atoms (@{thm nat_arith.add2}::path) y
-  | add_atoms path (Const (\<^const_name>\<open>Nat.Suc\<close>, _) $ x) =
+  | add_atoms path \<^Const_>\<open>Suc for x\<close> =
       add_atoms (@{thm nat_arith.suc1}::path) x
-  | add_atoms _ (Const (\<^const_name>\<open>Groups.zero\<close>, _)) = I
+  | add_atoms _ \<^Const_>\<open>Groups.zero _\<close> = I
   | add_atoms path x = cons (x, path)
 
 fun atoms t = add_atoms [] t []