src/HOL/MicroJava/ROOT.ML

handle Type.TYPE_MATCH, not arbitrary exceptions via MATCH_TYPE variable;
clarified handle/raise wrt. Quotient_Info.NotFound -- avoid fragile unqualified NotFound depending on "open" scope;
added helpful comments;

no_document use_thys ["While_Combinator"];

use_thys ["MicroJava"];