src/HOL/MicroJava/ROOT.ML

use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)

no_document use_thys ["While_Combinator"];

use_thys ["MicroJava"];