src/HOL/Nominal/Examples/ROOT.ML

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"];