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

added legacy type inference (from fixrec_package.ML);

simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements; simplified check_specification, read_specification: operate on a single list of simultaneous statements; tuned;

removed old named_spec, spec_name, spec_opt_name; clarified spec vs. specs; added alt_specs, where_alt_specs -- try to be robust against malformed input;