1.1 --- a/src/HOL/ex/ROOT.ML	Mon May 02 12:09:33 2011 +0200
     1.2 +++ b/src/HOL/ex/ROOT.ML	Mon May 02 13:29:47 2011 +0200
     1.3 @@ -11,7 +11,8 @@
     1.4    "Normalization_by_Evaluation",
     1.5    "Hebrew",
     1.6    "Chinese",
     1.7 -  "Serbian"
     1.8 +  "Serbian",
     1.9 +  "TPTP_Export"
    1.10  ];
    1.11  
    1.12  use_thys [
    1.13 @@ -78,7 +79,7 @@
    1.14  ];
    1.15  
    1.16  Unsynchronized.setmp Proofterm.proofs (! Proofterm.proofs)
    1.17 -  use_thy "CASC_THF0";
    1.18 +  use_thy "CASC_Setup";
    1.19  
    1.20  if getenv "ISABELLE_GHC" = "" then ()
    1.21  else use_thy "Quickcheck_Narrowing_Examples";