src/HOL/ex/ROOT.ML

   "List_to_Set_Comprehension_Examples",
   "Set_Algebras"
 ];
 
 Unsynchronized.setmp Proofterm.proofs (! Proofterm.proofs)
-  use_thy "TPTP";
+  use_thy "CASC_THF0";
 
 if getenv "ISABELLE_GHC" = "" then ()
 else use_thy "Quickcheck_Narrowing_Examples";
 
 use_thy "SVC_Oracle";