removed legacy_infer_term, legacy_infer_prop; modernized naming conventions: foo vs. foo_cmd; simplified preparation and outer parsing of specification; simplified command syntax setup;

old name_spec for 'axioms' and 'defs' (from spec_parse.ML);

added legacy type inference (from fixrec_package.ML);