diff -r 3e55334ef5af -r 21e042eee085 src/HOL/Data_Structures/Interval_Tree.thy
--- a/src/HOL/Data_Structures/Interval_Tree.thy	Sun Dec 01 21:14:56 2024 +0100
+++ b/src/HOL/Data_Structures/Interval_Tree.thy	Mon Dec 02 12:38:27 2024 +0100
@@ -73,12 +73,12 @@
 "max_hi Leaf = bot" |
 "max_hi (Node _ (_,m) _) = m"
 
-definition max3 :: "('a::linorder) ivl \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
-"max3 a m n = max (high a) (max m n)"
+definition max3 :: "('a::{linorder,order_bot}) ivl \<Rightarrow> 'a ivl_tree \<Rightarrow> 'a ivl_tree \<Rightarrow> 'a" where
+"max3 a l r = max (high a) (max (max_hi l) (max_hi r))"
 
 fun inv_max_hi :: "('a::{linorder,order_bot}) ivl_tree \<Rightarrow> bool" where
 "inv_max_hi Leaf \<longleftrightarrow> True" |
-"inv_max_hi (Node l (a, m) r) \<longleftrightarrow> (m = max3 a (max_hi l) (max_hi r) \<and> inv_max_hi l \<and> inv_max_hi r)"
+"inv_max_hi (Node l (a, m) r) \<longleftrightarrow> (m = max3 a l r \<and> inv_max_hi l \<and> inv_max_hi r)"
 
 lemma max_hi_is_max:
   "inv_max_hi t \<Longrightarrow> a \<in> set_tree t \<Longrightarrow> high a \<le> max_hi t"
@@ -119,7 +119,7 @@
 subsection \<open>Insertion and Deletion\<close>
 
 definition node where
-[simp]: "node l a r = Node l (a, max3 a (max_hi l) (max_hi r)) r"
+[simp]: "node l a r = Node l (a, max3 a l r) r"
 
 fun insert :: "'a::{linorder,order_bot} ivl \<Rightarrow> 'a ivl_tree \<Rightarrow> 'a ivl_tree" where
 "insert x Leaf = Node Leaf (x, high x) Leaf" |