src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Thu Aug 07 20:33:28 2025 +0200
+++ b/src/HOL/HOL.thy	Thu Aug 07 21:40:03 2025 +0200
@@ -2185,7 +2185,8 @@
 
   local
     val nnf_ss =
-      simpset_of (put_simpset HOL_basic_ss \<^context> addsimps @{thms simp_thms nnf_simps});
+      simpset_of (put_simpset HOL_basic_ss \<^context>
+        |> Simplifier.add_simps @{thms simp_thms nnf_simps});
   in
     fun nnf_conv ctxt = Simplifier.rewrite (put_simpset nnf_ss ctxt);
   end