Make parsing/testing slightly more efficient by using a heap.
Rework mmlPtreeConversion$ptree_Type to feature less case-splitting.

A few asserts and if-then-elses remove the need to case split on all
possible token forms, of which there are too many to make this
comfortable.

Really the issue is that the SML programmer writes

   case x of
     Form1(x) => something
   | _ => something else

and is happy that the program is small. When the HOL programmer does
the same, the resulting program (term) may not be small at all, even
if the input string is.