src/HOL/ex/ROOT.ML

--- a/src/HOL/ex/ROOT.ML	Mon May 02 12:09:33 2011 +0200
+++ b/src/HOL/ex/ROOT.ML	Mon May 02 13:29:47 2011 +0200
@@ -11,7 +11,8 @@
   "Normalization_by_Evaluation",
   "Hebrew",
   "Chinese",
-  "Serbian"
+  "Serbian",
+  "TPTP_Export"
 ];
 
 use_thys [
@@ -78,7 +79,7 @@
 ];
 
 Unsynchronized.setmp Proofterm.proofs (! Proofterm.proofs)
-  use_thy "CASC_THF0";
+  use_thy "CASC_Setup";
 
 if getenv "ISABELLE_GHC" = "" then ()
 else use_thy "Quickcheck_Narrowing_Examples";