marked some CRITICAL sections;
eliminated transform_failure (to avoid critical section for main transactions);
removed unused exceptions MetaSimplifier.SIMPROC_FAIL, Attrib.ATTRIB_FAIL, Method.METHOD_FAIL, Antiquote.ANTIQUOTE_FAIL;
use "../settings.ML";
no_document use_thy "While_Combinator";
use_thy "simp";
use_thy "WFrec";
use_thy "Partial";