made smlnj happy

more antiquotations;

more antiquotations; eliminated legacy ML bindings;

modernized structure Term_Ord;

use existing Typ_Graph;

further standard instances of functor Graph;

code simplification by inlining;

just one copy of structure Term_Graph (in Pure);

modernized structure Int_Graph;

clarified @{const_name} vs. @{const_abbrev};

clarified @{const_name} (only logical consts) vs. @{const_abbrev}; tuned;

type/const name: explicitly allow abbreviations as well;

clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;

added at-poly-test, which is intended for performance tests of Poly/ML itself;

more precise syntax antiquotations;

ML antiquotations for type classes;

read_class: perform actual read, with source position;

parallel brute-force disambiguation;

degrade gracefully in CRITICAL section;

gen_dest_case: recovered @{const_name} from c8a6fae0ad0c, because of separate Syntax.mark_const in case_tr' -- avoid extra syntax markers in output;

tuned;

use simplified Syntax.escape;

tuned hyp_subst_tac';

use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes

merged

more work on the new monotonicity stuff in Nitpick

improved precision of infinite "shallow" datatypes in Nitpick; e.g. strings used for variable names, instead of an opaque type

cosmetics

merged

merged