SML structure for ordered lists

[ordinarymath]

Right now Dep and Tag are implemented using ordered lists. However their merge operator doesn't take care to prevent allocation of new lists when the two lists are pointer eq. This issue is about is about defining a single structure containing functions operating on ordered lists. Isabelle has an implementation in src/Pure/General/ord_list.ML which could be ported over.