src/HOL/Tools/Sledgehammer/sledgehammer_run.ML

         val state' =
           if Config.get ctxt sledgehammer_result_request then
             state |> Proof.map_context
               (Config.put sledgehammer_result (quote name ^ ": " ^ message ()))
           else
-            ((if outcome_code = someN orelse mode = Normal then
+            ((if outcome_code = someN orelse mode = Normal orelse mode = Normal_Result then
                quote name ^ ": " ^ message ()
              else
                "")
               |> Async_Manager.break_into_chunks
               |> List.app Output.urgent_message;

       fun launch_atps_and_smt_solvers () =
         [launch_full_atps, launch_smts, launch_ueq_atps]
         |> Par_List.map (fn f => ignore (f (unknownN, state)))
         handle ERROR msg => (print ("Error: " ^ msg); error msg)
       fun maybe f (accum as (outcome_code, _)) =
-        accum |> (mode = Normal orelse outcome_code <> someN) ? f
+        accum |> (mode = Normal orelse mode = Normal_Result orelse outcome_code <> someN) ? f
     in
       (unknownN, state)
       |> (if blocking then
             launch_full_atps
             #> mode <> Auto_Try ? (maybe launch_ueq_atps #> maybe launch_smts)