use strict Global_Theory.register_proofs as checkpoint for stored zproof, and thus reduce current zboxes;

clarified signature;

omit pointless future: proof terms are built sequentially;

omit unclear / inaccurate renaming;

more normalization: re-use Thm.solve_constraints as important checkpoint for results, notably Global_Theory.name_thm;

more robust: avoid assumption about Context.certificate_theory;

tuned;

clarified pro-forma proof: no zboxes here (partially revert 686b7b14d041);

tuned;

tuned;