src/HOL/Auth/Shared.thy

--- a/src/HOL/Auth/Shared.thy	Thu Aug 07 20:33:28 2025 +0200
+++ b/src/HOL/Auth/Shared.thy	Thu Aug 07 21:40:03 2025 +0200
@@ -218,9 +218,9 @@
 
 val analz_image_freshK_ss =
   simpset_of
-   (\<^context> delsimps @{thms image_insert image_Un}
-      delsimps @{thms imp_disjL}    (*reduces blow-up*)
-      addsimps @{thms analz_image_freshK_simps})
+   (\<^context> |> Simplifier.del_simps @{thms image_insert image_Un}
+      |> Simplifier.del_simps @{thms imp_disjL}    (*reduces blow-up*)
+      |> Simplifier.add_simps @{thms analz_image_freshK_simps})
 
 end
 \<close>