slightly more explicit error, without going into the graph of proof futures;

proper transfer for Thm.derivation_name;

more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;

determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);

clarified signature;

clarified signature;

proof boxes based on proof digest (not proof term): thus it works with prune_proofs;

clarified files;

--HG--
rename : src/Pure/Thy/thm_deps.ML => src/Pure/thm_deps.ML