src/HOL/Tools/Sledgehammer/sledgehammer_run.ML

     else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
 
 fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, slice,
                               timeout, expect, ...})
         mode output_result minimize_command only learn
-        {state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name =
+        {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 |> the_default one_day)
     val _ = spying spy (fn () => (state, subgoal, name, "Launched"));

     val num_facts = length facts |> not only ? Integer.min max_facts
 
     fun desc () = prover_description ctxt params name num_facts subgoal subgoal_count goal
 
     val problem =
-      {state = state, goal = goal, subgoal = subgoal,
+      {comment = comment, state = state, goal = goal, subgoal = subgoal,
        subgoal_count = subgoal_count,
        factss = factss
          |> map (apsnd ((not (is_ho_atp ctxt name)
                          ? filter_out (fn ((_, (_, Induction)), _) => true
                                         | _ => false))

 
       fun launch_provers state label is_appropriate_prop provers =
         let
           val factss = get_factss label is_appropriate_prop provers
           val problem =
-            {state = state, goal = goal, subgoal = i, subgoal_count = n,
+            {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
              factss = factss}
           fun learn prover =
             mash_learn_proof ctxt params prover (prop_of goal) all_facts
           val launch =
             launch_prover params mode output_result minimize_command only learn