src/HOL/Tools/Sledgehammer/sledgehammer.ML

         try_methss [] methss
       end
   end
 
 fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, minimize, timeout,
-      preplay_timeout, expect, ...}) mode output_result only learn
+      preplay_timeout, expect, ...}) mode writeln_result only learn
     {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name =
   let
     val ctxt = Proof.context_of state
 
     val hard_timeout = time_mult 3.0 timeout

       let
         val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()
         val outcome =
           if outcome_code = someN orelse mode = Normal then quote name ^ ": " ^ message () else ""
         val _ =
-          if outcome <> "" andalso is_some output_result then
-            the output_result outcome
+          if outcome <> "" andalso is_some writeln_result then
+            the writeln_result outcome
           else
             outcome
             |> Async_Manager_Legacy.break_into_chunks
             |> List.app writeln
       in (outcome_code, []) end

   else
     cat_lines (map (fn (filter, facts) =>
       (if filter = "" then "" else quote filter ^ ": ") ^ string_of_facts facts) factss)
 
 fun run_sledgehammer (params as {verbose, spy, blocking, provers, max_facts, ...}) mode
-    output_result i (fact_override as {only, ...}) state =
+    writeln_result i (fact_override as {only, ...}) state =
   if null provers then
     error "No prover is set."
   else
     (case subgoal_count state of
       0 =>
       ((if blocking then error else writeln) "No subgoal!"; (false, (noneN, [])))
     | n =>
       let
         val _ = Proof.assert_backward state
         val print =
-          if mode = Normal andalso is_none output_result then writeln else K ()
+          if mode = Normal andalso is_none writeln_result then writeln else K ()
         val ctxt = Proof.context_of state
         val keywords = Thy_Header.get_keywords' ctxt
         val {facts = chained, goal, ...} = Proof.goal state
         val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
         val ho_atp = exists (is_ho_atp ctxt) provers

             val factss = get_factss provers
             val problem =
               {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
                factss = factss}
             val learn = mash_learn_proof ctxt params (Thm.prop_of goal) all_facts
-            val launch = launch_prover params mode output_result only learn
+            val launch = launch_prover params mode writeln_result only learn
           in
             if mode = Auto_Try then
               (unknownN, [])
               |> fold (fn prover => fn accum as (outcome_code, _) =>
                   if outcome_code = someN then accum else launch problem prover)