Worklist.CMakeSourcePriority queues with generated comparison function. Added benefit: insertion at the front/rear can be guaranteed. Culprit: does not behave as a set (i.e. the same element of X.t w.r.t to = can be inserted twice in the queue).