Imported my new, optimized AVL tree implementation (still based on the code generated from the Isabelle-HOL theory).
Modified the existing code as necessary to work with the new AVL tree.
Moved the helper functions for union, intersection, and difference out into the module so they're easier to work with.
Minor tweaks; added a TODO comment about a small improvement we could make to the balanced DIET algorithm in the future.
Made some simplifications to the Join and Reroot methods of AvlTree.
Added some comments within the code to help understand what the code is doing.
Temporarily re-implemented 'union' using AvlTree.Fold; interestingly, this still triggers the bug, so that drastically lowers the number of places to look for it.
Fixed the assertion in the Diet.difference function -- the minimum number of elements in the result is always 0, so we should be checking for a maximum number of elements.
Removed unused, duplicate 'split' function.
Created a balanceTolerance constant and modified the code to use it; adjusting it from 2 to 1 still results in triggering the assertion in union, but the assertion message indicates that lowering the tolerance brings the expected and actual values closer together.