simplify code

prevent schematic variable clash in combinator-introduction code, when invoked from Sledgehammer (another consequence of the CNF -> FOF transition)

remove obsolete field in record

simplify code

get rid of obsolete "axiom ID" component, since it's now always 0

reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting

added extensionalization to Sledgehammer, mimicking what the Clausifier used to do

simplify code

remove more Skolemization-aware code

kill Skolem handling in Sledgehammer

simplify "conjecture_shape" business, as a result of using FOF instead of CNF

generate full first-order formulas (FOF) in Sledgehammer

make TPTP generator accept full first-order formulas

generate close formulas for SPASS, but not for the others (to avoid clutter)

renamed internal function

proof reconstruction for full FOF terms

remove confusing line in SPASS output (because the axiom names are off -- bug in SPASS)

reorder SPASS conjectures correctly, based on Flotter output

Deleted an obsolete file

explicit Keyword.control markup for various control commands -- to prevent them from occurring in proof documents;

use file names relative to master directory of theory source -- Proof General can now handle that due to the ThyLoad.add_path deception (cf. 3ceccd415145);

simplified handling of update_time -- do not store within deps;

clarified register_thy: clean slate via kill_thy, more precise CRITICAL section; tuned;

updated keywords;