fixed a printing problem for bounded quantifiers and bounded set operators in the case of tuples

moved some configurations to AFP, and fixed others

more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;

enable inner syntax source positions by default (controlled via configuration option); disable source positions for HOLCF, due to special pattern translations;

binder_tr: more informative exception;

Hoare syntax: strip positions where they crash translation functions; re-unified some clones (!);

update_name_tr: more precise handling of explicit constraints, including positions;

statespace syntax: strip positions -- type constraints are unexpected here;

let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);

datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";

tuned indendation and parentheses;

support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive; simplified/generalized abs_tr/binder_tr: allow iterated constraints, stemming from positions; Ast.pretty_ast: special treatment of encoded positions; eliminated Ast.str_of_ast in favour of uniform Ast.pretty_ast;

pretty_string: proper handling of negative max_len;

added Lexicon.encode_position, Lexicon.decode_position;

tuned;

tuned;

clarified Syn_Trans.parsetree_to_ast and Syn_Trans.ast_to_term;

tuned;

merged

added judgement day configurations

another attempt to exec ISABELLE_GHC robustly (cf. d8c3b26b3da4, 994d088fbfbc);

fixed perl error

eliminated unnecessary generated ROOT.ML

more precise dependencies