--- a/src/HOL/Computational_Algebra/Polynomial.thy	Fri Jun 06 18:36:29 2025 +0100
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Mon Jun 09 22:14:38 2025 +0200
@@ -550,7 +550,7 @@
   where [code]: "is_zero p \<longleftrightarrow> List.null (coeffs p)"
 
 lemma is_zero_null [code_abbrev]: "is_zero p \<longleftrightarrow> p = 0"
-  by (simp add: is_zero_def null_def)
+  by (simp add: is_zero_def)
 
 
 text \<open>Reconstructing the polynomial from the list\<close>