updated keywords;

replaced old Sign.add_tyabbrs(_i) by Sign.add_type_abbrev (without mixfix); misc tuning and simplification;

keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;

separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';

replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;

allow syntax types within abbreviations;

modernized old-style type abbreviations;

modernized type abbreviations;

local type abbreviations;

merged

added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)

store nonmangled names along with mangled type names in Sledgehammer for debugging purposes

give more sensible names to "fol_type" constructors, as requested by a FIXME comment

make Sledgehammer's output more debugging friendly

made SML/NJ happy;

proper masking of dummy name_space;

salvaged some ML functors from decay, which is the natural consequence of lack of formal checking;

proper checking of ML functors (in Poly/ML 5.2 or later); eliminated pathetic comments;

added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;

isatest: improved treatment of local files on atbroy102;

add rule deflation_ID to proof script for take + constructor rules

more robust record syntax: use Type.raw_match to ignore sort constraints as in regular abbreviations (also note that constraints only affect operations, not types);

HOL record: explicitly allow sort constraints;

misc tuning and simplification;

explicit ProofContext.check_tfree;

merged

Respectfullness and preservation of list_rel

replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo; simplified via ProofContext.check_tfree;

get_sort: suppress dummyS from input; added check_tvar, check_tfree convenience; tuned;

modernized treatment of sort constraints in specification; pass-through type variables as usual as (string * sort) internally -- recovers proper sort handling;