src/HOL/ROOT.ML

make sure short theorem names are preferred to composite ones in Sledgehammer;
this code used to work at some point

(* Classical Higher-order Logic -- batteries included *)

use_thys ["Complex_Main"];