expand hard tabs;
proper configuration option "ML_print_depth"; proper ML_exception_trace for HOL-TPTP;
more portable hash-bang;
split make_tptp_parser into two scripts, for parser and lib respectively;