don't use readable names if proof reconstruction is needed, because it uses the structure of names

--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Mon Apr 19 11:02:00 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Mon Apr 19 11:54:07 2010 +0200
@@ -128,7 +128,7 @@
       if Config.get ctxt measure_runtime then split_time s else (s, 0)
     fun run_on probfile =
       if File.exists cmd then
-        write_file debug full_types probfile clauses
+        write_file full_types probfile clauses
         |> pair (apfst split_time' (bash_output (cmd_line probfile)))
       else error ("Bad executable: " ^ Path.implode cmd ^ ".");
 
@@ -176,7 +176,8 @@
       (get_relevant_facts respect_no_atp relevance_threshold convergence
                           higher_order follow_defs max_new_clauses
                           (the_default prefers_theory_relevant theory_relevant))
-      (prepare_clauses higher_order false) write_tptp_file command
+      (prepare_clauses higher_order false)
+      (write_tptp_file (overlord andalso not isar_proof)) command
       (arguments timeout) failure_strs
       (if supports_isar_proofs andalso isar_proof then
          structured_isar_proof modulus sorts

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Apr 19 11:02:00 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Apr 19 11:54:07 2010 +0200
@@ -220,7 +220,8 @@
 type name = string * string
 type name_pool = string Symtab.table * string Symtab.table
 
-fun empty_name_pool debug = if debug then SOME (`I Symtab.empty) else NONE
+fun empty_name_pool readable_names =
+  if readable_names then SOME (`I Symtab.empty) else NONE
 
 fun pool_map f xs =
   fold_rev (fn x => fn (ys, pool) => f x pool |>> (fn y => y :: ys)) xs
@@ -242,7 +243,7 @@
 fun translate_first_char f s =
   String.str (f (String.sub (s, 0))) ^ String.extract (s, 1, NONE)
 
-fun clean_short_name full_name s =
+fun readable_name full_name s =
   let
     val s = s |> Long_Name.base_name
               |> fold remove_all ["\<^sub>", "\<^bsub>", "\<^esub>", "\<^isub>"]
@@ -270,8 +271,8 @@
   | nice_name (full_name, desired_name) (SOME the_pool) =
     case Symtab.lookup (fst the_pool) full_name of
       SOME nice_name => (nice_name, SOME the_pool)
-    | NONE => add_nice_name full_name (clean_short_name full_name desired_name)
-                            0 the_pool
+    | NONE => add_nice_name full_name (readable_name full_name desired_name) 0
+                            the_pool
               |> apsnd SOME
 
 (**** Definitions and functions for FOL clauses, for conversion to TPTP or DFG

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Apr 19 11:02:00 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Apr 19 11:54:07 2010 +0200
@@ -38,7 +38,7 @@
     hol_clause list * hol_clause list * hol_clause list * hol_clause list *
     classrel_clause list * arity_clause list ->
     int * int
-  val write_dfg_file : bool -> bool -> Path.T ->
+  val write_dfg_file : bool -> Path.T ->
     hol_clause list * hol_clause list * hol_clause list * hol_clause list *
     classrel_clause list * arity_clause list -> int * int
 end
@@ -479,11 +479,11 @@
 
 (* TPTP format *)
 
-fun write_tptp_file debug full_types file clauses =
+fun write_tptp_file readable_names full_types file clauses =
   let
     fun section _ [] = []
       | section name ss = "\n% " ^ name ^ plural_s (length ss) ^ "\n" :: ss
-    val pool = empty_name_pool debug
+    val pool = empty_name_pool readable_names
     val (conjectures, axclauses, _, helper_clauses,
       classrel_clauses, arity_clauses) = clauses
     val (cma, cnh) = count_constants clauses
@@ -512,7 +512,7 @@
 
 (* DFG format *)
 
-fun write_dfg_file debug full_types file clauses =
+fun write_dfg_file full_types file clauses =
   let
     (* Some of the helper functions below are not name-pool-aware. However,
        there's no point in adding name pool support if the DFG format is on its