diff -r daa604a00491 -r 3eda814762fc src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Thu Aug 08 18:56:14 2024 +0100
+++ b/src/HOL/Library/Float.thy	Fri Aug 09 20:45:31 2024 +0100
@@ -849,7 +849,7 @@
     have "real_of_int \<lfloor>real_of_int a / real_of_int b\<rfloor> \<le> real_of_int a / real_of_int b"
       by simp
     moreover have "real_of_int \<lfloor>real_of_int a / real_of_int b\<rfloor> \<noteq> real_of_int a / real_of_int b"
-      by (smt (verit) floor_divide_of_int_eq ne real_of_int_div_aux)
+      by (smt (verit) floor_divide_of_int_eq ne of_int_div_aux)
     ultimately show "real_of_int \<lfloor>real_of_int a / real_of_int b\<rfloor> < real_of_int a / real_of_int b" by arith
   qed
   then show ?thesis