--- a/src/HOL/Probability/SPMF.thy	Fri Mar 14 18:04:14 2025 +0100
+++ b/src/HOL/Probability/SPMF.thy	Fri Mar 14 18:11:38 2025 +0100
@@ -1482,7 +1482,7 @@
 next
   fix x y z
   assume "?R x y" "?R y z"
-  with transp_ord_option[OF transp_equality] show "?R x z" by(rule transp_rel_pmf[THEN transpD])
+  with transp_ord_option[OF transp_on_equality] show "?R x z" by(rule transp_rel_pmf[THEN transpD])
 next
   fix x y
   assume "?R x y" "?R y x"