make sure short theorem names are preferred to composite ones in Sledgehammer;
this code used to work at some point
(* Title: HOL/Metis_Examples/ROOT.ML
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Testing the metis method.
*)
use_thys ["set", "BigO", "Abstraction", "BT", "Message", "Tarski", "TransClosure"];