src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

      timeout : Time.time option,
      preplay_timeout : Time.time option,
      expect : string}
 
   type prover_problem =
-    {state : Proof.state,
+    {comment : string,
+     state : Proof.state,
      goal : thm,
      subgoal : int,
      subgoal_count : int,
      factss : (string * fact list) list}
 

    timeout : Time.time option,
    preplay_timeout : Time.time option,
    expect : string}
 
 type prover_problem =
-  {state : Proof.state,
+  {comment : string,
+   state : Proof.state,
    goal : thm,
    subgoal : int,
    subgoal_count : int,
    factss : (string * fact list) list}
 

         (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
                     uncurried_aliases, fact_filter, max_facts, max_mono_iters,
                     max_new_mono_instances, isar_proofs, isar_compress,
                     isar_try0, slice, timeout, preplay_timeout, ...})
         minimize_command
-        ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
+        ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
     val atp_mode =
       if Config.get ctxt completish then Sledgehammer_Completish

               "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")"
               |> enclose "TIMEFORMAT='%3R'; { time " " ; }"
             val _ =
               atp_problem
               |> lines_of_atp_problem format ord ord_info
-              |> cons ("% " ^ command ^ "\n")
+              |> cons ("% " ^ command ^ "\n" ^
+                (if comment = "" then "" else "% " ^ comment ^ "\n"))
               |> File.write_list prob_path
             val ((output, run_time), (atp_proof, outcome)) =
               time_limit generous_slice_timeout Isabelle_System.bash_output
                          command
               |>> (if overlord then