minor changes to meta-prover
in Type, curried constructors with better names (arrow/arrow_list)
updated type inference, Signature and HOTerm to use the new Type arrows
use ParseLocation.of_lexbuf in parsers;
Parse_ho and Parse_tptp now use specific constructors to transform the AST,
especially for polymorphic operators such as =, so that missing type vars
or surrouding arguments with multisets is done at parse time
update detect_theories