diff -r cccbfa567117 -r b69e4da2604b src/HOL/Import/HOL_Light_Maps.thy
--- a/src/HOL/Import/HOL_Light_Maps.thy	Fri Jun 06 18:36:29 2025 +0100
+++ b/src/HOL/Import/HOL_Light_Maps.thy	Mon Jun 09 22:14:38 2025 +0200
@@ -286,7 +286,7 @@
 
 lemma NULL[import_const NULL : List.null]:
   "List.null ([]::'t18373 list) = True \<and> List.null ((h::'t18373) # t) = False"
-  unfolding null_def by simp
+  by simp
 
 lemma ALL[import_const ALL : list_all]:
   "list_all (P::'t18393 \<Rightarrow> bool) [] = True \<and>