diff -r 55a71dd13ca0 -r 73af47bc277c 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