use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing

--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Tue Jun 07 10:46:09 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Tue Jun 07 11:04:17 2011 +0200
@@ -42,7 +42,6 @@
     Proof.context -> type_sys -> int list list -> int
     -> (string * locality) list vector -> 'a proof -> string list option
   val uses_typed_helpers : int list -> 'a proof -> bool
-  val reconstructor_name : reconstructor -> string
   val one_line_proof_text : one_line_params -> string
   val make_tvar : string -> typ
   val make_tfree : Proof.context -> string -> typ
@@ -254,10 +253,10 @@
 (** Soft-core proof reconstruction: Metis one-liner **)
 
 (* unfortunate leaking abstraction *)
-fun reconstructor_name Metis = "metis"
-  | reconstructor_name Metis_Full_Types = "metis (full_types)"
-  | reconstructor_name Metis_No_Types = "metis (no_types)"
-  | reconstructor_name (SMT _) = "smt"
+fun name_of_reconstructor Metis = "metis"
+  | name_of_reconstructor Metis_Full_Types = "metis (full_types)"
+  | name_of_reconstructor Metis_No_Types = "metis (no_types)"
+  | name_of_reconstructor (SMT _) = "smt"
 
 fun reconstructor_settings (SMT settings) = settings
   | reconstructor_settings _ = ""
@@ -283,7 +282,7 @@
 fun reconstructor_command reconstructor i n (ls, ss) =
   using_labels ls ^
   apply_on_subgoal (reconstructor_settings reconstructor) i n ^
-  command_call (reconstructor_name reconstructor) ss
+  command_call (name_of_reconstructor reconstructor) ss
 fun minimize_line _ [] = ""
   | minimize_line minimize_command ss =
     case minimize_command ss of

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 10:46:09 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 11:04:17 2011 +0200
@@ -10,10 +10,11 @@
 sig
   type failure = ATP_Proof.failure
   type locality = ATP_Translate.locality
-  type relevance_fudge = Sledgehammer_Filter.relevance_fudge
   type type_sys = ATP_Translate.type_sys
+  type reconstructor = ATP_Reconstruct.reconstructor
   type play = ATP_Reconstruct.play
   type minimize_command = ATP_Reconstruct.minimize_command
+  type relevance_fudge = Sledgehammer_Filter.relevance_fudge
 
   datatype mode = Auto_Try | Try | Normal | Minimize
 
@@ -79,6 +80,7 @@
   val smt_slice_min_secs : int Config.T
   val das_tool : string
   val select_smt_solver : string -> Proof.context -> Proof.context
+  val prover_name_for_reconstructor : reconstructor -> string option
   val is_metis_prover : string -> bool
   val is_atp : theory -> string -> bool
   val is_smt_prover : Proof.context -> string -> bool
@@ -137,13 +139,15 @@
    (metis_full_typesN, Metis_Full_Types),
    (metis_no_typesN, Metis_No_Types)]
 
+val prover_name_for_reconstructor =
+  AList.find (op =) metis_prover_infos #> try hd
+
 val metis_reconstructors = map snd metis_prover_infos
 
 val is_metis_prover = AList.defined (op =) metis_prover_infos
 val is_atp = member (op =) o supported_atps
 
-val select_smt_solver =
-  Context.proof_map o SMT_Config.select_solver
+val select_smt_solver = Context.proof_map o SMT_Config.select_solver
 
 fun is_smt_prover ctxt name =
   member (op =) (SMT_Solver.available_solvers_of ctxt) name
@@ -531,9 +535,7 @@
   (case preplay of
      Played (reconstructor, time) =>
      if Time.<= (time, metis_minimize_max_time) then
-       case AList.find (op =) metis_prover_infos reconstructor of
-         metis_name :: _ => metis_name
-       | [] => name
+       prover_name_for_reconstructor reconstructor |> the_default name
      else
        name
    | _ => name)
@@ -875,14 +877,14 @@
   let
     val max_slices = if slicing then Config.get ctxt smt_max_slices else 1
     val repair_context =
-          select_smt_solver name
-          #> (if overlord then
-                Config.put SMT_Config.debug_files
-                           (overlord_file_location_for_prover name
-                            |> (fn (path, name) => path ^ "/" ^ name))
-              else
-                I)
-          #> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
+      select_smt_solver name
+      #> (if overlord then
+            Config.put SMT_Config.debug_files
+                       (overlord_file_location_for_prover name
+                        |> (fn (path, name) => path ^ "/" ^ name))
+          else
+            I)
+      #> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
     val state = state |> Proof.map_context repair_context
     fun do_slice timeout slice outcome0 time_so_far facts =
       let

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Jun 07 10:46:09 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Jun 07 11:04:17 2011 +0200
@@ -102,7 +102,8 @@
                   (case preplay of
                      Played (reconstructor, timeout) =>
                      if can_min_fast_enough (Time.toMilliseconds timeout) then
-                       (true, reconstructor_name reconstructor)
+                       (true, prover_name_for_reconstructor reconstructor
+                              |> the_default name)
                      else
                        (prover_fast_enough, name)
                    | _ => (prover_fast_enough, name),