Improve or remove ALL_EL_CONV

[xrchz]

One would hope ListConv1.ALL_EL_CONV to be an efficient specialised conversion for evaluating EVERY _ _ terms, but it actually performs much worse than EVAL. If it can't be made to do better, I think it should be removed (or replaced by something that simply defers to computeLib).

Some more information from @mn200: Looking at ALL_EL_CONV’s implementation, it seems as if it will always traverse the entire list, and so won’t bottom out quickly if there is an element not satisfying the predicate. But it’s still slower than EVAL even if the predicate is true of every element.

One possible explanation for this is that ALL_EL_CONV calls dest_list to extract an ML list of the list’s elements. This is then used to build up a copy of the input list on the LHS of the final result theorem (through repeated calls to SPECL). This is clearly wasteful. Using Portable.pointer_eq, you can test to see if the term on the LHS of the resulting theorem is equal to the term originally used. With EVAL it is; with ALL_EL_CONV it isn’t.