diff -r 55a71dd13ca0 -r 73af47bc277c src/HOL/Analysis/normarith.ML
--- a/src/HOL/Analysis/normarith.ML	Thu Aug 07 20:33:28 2025 +0200
+++ b/src/HOL/Analysis/normarith.ML	Thu Aug 07 21:40:03 2025 +0200
@@ -386,7 +386,7 @@
 
   fun init_conv ctxt =
    Simplifier.rewrite (put_simpset HOL_basic_ss ctxt
-    addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm dist_norm}, @{thm right_minus},
+    |> Simplifier.add_simps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm dist_norm}, @{thm right_minus},
       @{thm diff_self}, @{thm norm_zero}] @ @{thms arithmetic_simps} @ @{thms norm_pths}))
    then_conv Numeral_Simprocs.field_comp_conv ctxt
    then_conv nnf_conv ctxt