clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b); uniform handling of exceptions in depth_tac and blast_tac, discontinued separate blast_depth_tac; tuned blast_tac: atomize prems only once, outside DEEPEN;

clarified special incr_type_indexes;

tuned signature: Name.invent and Name.invent_names;

modernized structure ProofContext;

even more robust \isaspacing;

simplified Name.variant -- discontinued builtin fold_map;