tuned
authornipkow
Mon, 03 May 2021 19:06:33 +0200
changeset 73875 0c8d6bec6491
parent 73874 4b413b78cd94
child 73876 58aed6f71f90
tuned
src/HOL/Data_Structures/Leftist_Heap.thy
--- a/src/HOL/Data_Structures/Leftist_Heap.thy	Sun May 02 21:46:59 2021 +0200
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Mon May 03 19:06:33 2021 +0200
@@ -37,8 +37,8 @@
 
 definition node :: "'a lheap \<Rightarrow> 'a \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
 "node l a r =
- (let rl = mht l; rr = mht r
-  in if rl \<ge> rr then Node l (a,rr+1) r else Node r (a,rl+1) l)"
+ (let mhl = mht l; mhr = mht r
+  in if mhl \<ge> mhr then Node l (a,mhr+1) r else Node r (a,mhl+1) l)"
 
 fun get_min :: "'a lheap \<Rightarrow> 'a" where
 "get_min(Node l (a, n) r) = a"