diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/Tools/cnf.ML
--- a/src/HOL/Tools/cnf.ML	Wed Jan 22 21:35:05 2025 +0100
+++ b/src/HOL/Tools/cnf.ML	Wed Jan 22 22:22:19 2025 +0100
@@ -106,7 +106,7 @@
     (* becomes "[..., A1, ..., An] |- B"                                   *)
     fun prems_to_hyps thm =
       fold (fn cprem => fn thm' =>
-        Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm
+        Thm.implies_elim thm' (Thm.assume cprem)) (Thm.cprems_of thm) thm
   in
     (* [...] |- ~(x1 | ... | xn) ==> False *)
     (@{thm cnf.clause2raw_notE} OF [clause])