pass token source to typ/term etc.;

added name property operation;
added local_fact;
renamed proposition to prop (again);

renamed ML_Lex.val_of to content_of;

unified Args.T with OuterLex.token, renamed some operations;
moved thm_sel to attrib.ML;

unified Args.T with OuterLex.token;
RESET_VALUE of primitive parsers;
export keyword_with;
renamed keyword_sid to keyword_ident_or_symbolic;
added int (from args.ML);
added enum(1)', and_list(1)' (formerly in args.ML);
removed obsolete arguments/generic_args1 (cf. parse/parse1 in args.ML);

unified Args.T with OuterLex.token;
renamed val_of to content_of;
added InternalValue kind;
added datatype value/slot with static binding (from args.ML);
renamed is_sid to ident_or_symbolic;

unified Args.T with OuterLex.token, renamed some operations;
removed obsolete parse_args (cf. parse);

unified Args.T with OuterLex.token, renamed some operations;
unified version of thm_sel (formerly in args.ML and spec_parse.ML);

unified Args.T with OuterLex.token;
moved datatype value/slot and basic operations to outer_lex.ML;
removed unused terminator;
removed obsolete !!!, position, nat, int, list(1), enum(1) and_list(1) (cf. outer_parse.ML);
removed obsolete thm_sel (cf. attrib.ML);
one unified version of parse/parse1 (formerly arguments/generic_args1 in outer_parse.ML);

load args.ML later (after outer_parse.ML);