# HG changeset patch # User nipkow # Date 1620061593 -7200 # Node ID 0c8d6bec6491291ab4eba0e45fff19da13bfc2b4 # Parent 4b413b78cd948f063e597be95f3570f151c822e4 tuned diff -r 4b413b78cd94 -r 0c8d6bec6491 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 \ 'a \ 'a lheap \ 'a lheap" where "node l a r = - (let rl = mht l; rr = mht r - in if rl \ 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 \ mhr then Node l (a,mhr+1) r else Node r (a,mhl+1) l)" fun get_min :: "'a lheap \ 'a" where "get_min(Node l (a, n) r) = a"