src/HOL/MicroJava/ROOT.ML

if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem

no_document use_thys ["While_Combinator"];

use_thys ["MicroJava"];