promise: include check into future body, i.e. joined results are always valid; pending future derivations: shared ref within whole theory body, i.e. end-of-theory joins *all* derivations ever forked from a version of the theory; simplified rep_deriv;

proper transfer of theorems that involve classes being instantiated here;

HOL_USEDIR_OPTIONS no longer applies to HOL-Plain (main HOL is rebuilt from Pure);