src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML

     SMT of string
 
   datatype preplay =
     Preplayed of reconstructor * Time.time |
     Trust_Playable of reconstructor * Time.time option|
-    Preplay_Failed
+    Failed_to_Preplay
 
   type minimize_command = string list -> string
   type one_line_params =
     preplay * string * (string * locality) list * minimize_command * thm * int
   type isar_params =

   SMT of string
 
 datatype preplay =
   Preplayed of reconstructor * Time.time |
   Trust_Playable of reconstructor * Time.time option |
-  Preplay_Failed
+  Failed_to_Preplay
 
 type minimize_command = string list -> string
 type one_line_params =
   preplay * string * (string * locality) list * minimize_command * thm * int
 type isar_params =

   | reconstructor_settings _ = ""
 
 fun string_for_label (s, num) = s ^ string_of_int num
 
 fun show_time NONE = ""
-  | show_time (SOME ext_time) = " ~ " ^ string_from_ext_time ext_time
+  | show_time (SOME ext_time) = " (" ^ string_from_ext_time ext_time ^ ")"
 
 fun set_settings "" = ""
   | set_settings settings = "using [[" ^ settings ^ "]] "
 fun apply_on_subgoal settings _ 1 = set_settings settings ^ "by "
   | apply_on_subgoal settings 1 _ = set_settings settings ^ "apply "

         (SOME reconstructor,
          case time of
            NONE => NONE
          | SOME time =>
            if time = Time.zeroTime then NONE else SOME (true, time))
-      | Preplay_Failed => (NONE, NONE)
+      | Failed_to_Preplay => (NONE, NONE)
     val n = Logic.count_prems (prop_of goal)
     val try_line =
       case reconstructor of
         SOME r => reconstructor_command r i n ([], map fst extra)
                   |> try_command_line banner ext_time

         |> the_default "\nWarning: The Isar proof construction failed."
   in one_line_proof ^ isar_proof end
 
 fun proof_text ctxt isar_proof isar_params
                (one_line_params as (preplay, _, _, _, _, _)) =
-  (if isar_proof orelse preplay = Preplay_Failed then
+  (if isar_proof orelse preplay = Failed_to_Preplay then
      isar_proof_text ctxt isar_params
    else
      one_line_proof_text) one_line_params
 
 end;