src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

                    choose_minimize_command ctxt params minimize_command name
                                            preplay,
                    subgoal, subgoal_count)
                 val num_chained = length (#facts (Proof.goal state))
               in
-                proof_text ctxt isar_proofs isar_params num_chained
+                proof_text ctxt (mode = Auto_Try) isar_proofs isar_params num_chained
                            one_line_params
               end,
            (if verbose then
               "\nATP real CPU time: " ^ string_of_time run_time ^ "."
             else

                 (preplay, proof_banner mode name, used_facts,
                  choose_minimize_command ctxt params minimize_command name
                                          preplay,
                  subgoal, subgoal_count)
               val num_chained = length (#facts (Proof.goal state))
-            in one_line_proof_text num_chained one_line_params end,
+            in one_line_proof_text (mode = Auto_Try) num_chained one_line_params end,
          if verbose then
            "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "."
          else
            "")
       | SOME failure =>

               val one_line_params =
                 (play, proof_banner mode name, used_facts,
                  minimize_command override_params name, subgoal,
                  subgoal_count)
               val num_chained = length (#facts (Proof.goal state))
-            in one_line_proof_text num_chained one_line_params end,
+            in one_line_proof_text (mode = Auto_Try) num_chained one_line_params end,
        message_tail = ""}
     | play =>
       let
         val failure = case play of Failed_to_Play _ => GaveUp | _ => TimedOut
       in