moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
theory loader: reduced warnings -- thy database can be bypassed in certain situations;
Proof/Local_Theory.propagate_ml_env;
ML use function: propagate ML environment as well;
pervasive type generic_theory;
use_thys ["Nominal_Examples"];
setmp_noncritical quick_and_dirty true use_thys ["VC_Condition"];