remove needless "-x" option, now that (1) we can't handle remote SPASS anymore; and (2) we can a priori parse the SPASS syntax in "Sledgehammer_Proof_Reconstruct" anyway
use_thy "FP0";
use_thy "FP1";
use_thy "RECDEF";
use_thy "Rules";
use_thy "Sets";
use_thy "Ind";