fix ROOT.ML and handle "readable_names" reference slightly more cleanly

--- 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";

--- a/src/HOL/ex/TPTP_Export.thy	Mon May 02 12:09:33 2011 +0200
+++ b/src/HOL/ex/TPTP_Export.thy	Mon May 02 13:29:47 2011 +0200
@@ -4,10 +4,16 @@
 begin
 
 ML {*
+val readable_names = !Sledgehammer_ATP_Translate.readable_names;
+Sledgehammer_ATP_Translate.readable_names := false
+*}
+
+ML {*
 val thy = @{theory Complex_Main}
 val ctxt = @{context}
 *}
 
+(*
 ML {*
 TPTP_Export.generate_tptp_inference_file_for_theory ctxt thy true
     "/tmp/infs_full_types.tptp"
@@ -22,5 +28,10 @@
 TPTP_Export.generate_tptp_graph_file_for_theory ctxt thy
     "/tmp/graph.out"
 *}
+*)
+
+ML {*
+Sledgehammer_ATP_Translate.readable_names := readable_names
+*}
 
 end

--- a/src/HOL/ex/tptp_export.ML	Mon May 02 12:09:33 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML	Mon May 02 13:29:47 2011 +0200
@@ -17,8 +17,6 @@
 structure TPTP_Export : TPTP_EXPORT =
 struct
 
-val _ = Sledgehammer_ATP_Translate.readable_names := false
-
 val ascii_of = Metis_Translate.ascii_of
 
 val fact_name_of = prefix Sledgehammer_ATP_Translate.fact_prefix o ascii_of