src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

   type fact = Sledgehammer_Fact.fact
   type reconstructor = Sledgehammer_Reconstructor.reconstructor
   type play = Sledgehammer_Reconstructor.play
   type minimize_command = Sledgehammer_Reconstructor.minimize_command
 
-  datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
+  datatype mode = Auto_Try | Try | Normal | Normal_Result | MaSh | Auto_Minimize | Minimize
 
   type params =
     {debug : bool,
      verbose : bool,
      overlord : bool,

 open Sledgehammer_Reconstruct
 
 
 (** The Sledgehammer **)
 
-datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
+datatype mode = Auto_Try | Try | Normal | Normal_Result | MaSh | Auto_Minimize | Minimize
 
 (* Identifier that distinguishes Sledgehammer from other tools that could use
    "Async_Manager". *)
 val SledgehammerN = "Sledgehammer"
 

          (max_new_instances |> the_default best_max_new_instances)
 
 fun suffix_of_mode Auto_Try = "_try"
   | suffix_of_mode Try = "_try"
   | suffix_of_mode Normal = ""
+  | suffix_of_mode Normal_Result = ""
   | suffix_of_mode MaSh = ""
   | suffix_of_mode Auto_Minimize = "_min"
   | suffix_of_mode Minimize = "_min"
 
 (* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on

       else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output
     val ((_, (_, pool, fact_names, lifted, sym_tab)),
          (output, run_time, used_from, atp_proof, outcome)) =
       with_cleanup clean_up run () |> tap export
     val important_message =
-      if mode = Normal andalso
+      if (mode = Normal orelse mode = Normal_Result) andalso
          random_range 0 (atp_important_message_keep_quotient - 1) = 0 then
         extract_important_message output
       else
         ""
     val (used_facts, preplay, message, message_tail) =