Fix OT build

[binghe]

Hi,

This PR fixes the OT building after type annotations on basic lisp theorems added in 409fbbf.

This time I sorted the goals retrieved from hol4-assums.art (generated by opentheory) so that if only the order of theorems changed, the sorted list should remain the same:

val goalsNet = read_article "hol4-assums.art" reader;
val goals_unsorted = Net.listItems goalsNet;
fun term_lt t1 t2 = (Term.compare(t1,t2) = LESS);
fun thm_lt th1 th2 = term_lt (concl th1) (concl th2);
val goals = sort thm_lt goals_unsorted;

As the result, the proofs of these goals are completely reordered, leading to large amount of code changes.

Chun

[mn200]

Thanks for this!