diff -r 6e85281177df -r 26a1d66b9077 src/HOL/Data_Structures/Interval_Tree.thy
--- a/src/HOL/Data_Structures/Interval_Tree.thy	Mon May 10 14:28:37 2021 +0200
+++ b/src/HOL/Data_Structures/Interval_Tree.thy	Mon May 10 16:14:34 2021 +0200
@@ -50,7 +50,7 @@
   show b: "x \<le> x"
     by (simp add: ivl_less_eq)
   show c: "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
-    by (smt ivl_less_eq dual_order.trans less_trans)
+    using ivl_less_eq by fastforce
   show d: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
     using ivl_less_eq a ivl_inj ivl_less by fastforce
   show e: "x \<le> y \<or> y \<le> x"