src/HOL/Tools/ATP_Manager/atp_manager.ML

   val info: unit -> unit
   val messages: int option -> unit
   type prover = int -> (thm * (string * int)) list option ->
     (thm * (string * int)) list option -> string -> int ->
     Proof.context * (thm list * thm) ->
-    bool * string * string * string vector * (thm * (string * int)) list
+    bool * (string * string list) * string * string vector * (thm * (string * int)) list
   val add_prover: string -> prover -> theory -> theory
   val print_provers: theory -> unit
   val get_prover: string -> theory -> prover option
   val sledgehammer: string list -> Proof.state -> unit
 end;

 (* named provers *)
 
 type prover = int -> (thm * (string * int)) list option ->
   (thm * (string * int)) list option -> string -> int ->
   Proof.context * (thm list * thm) ->
-  bool * string * string * string vector * (thm * (string * int)) list
+  bool * (string * string list) * string * string vector * (thm * (string * int)) list
 
 fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
 
 structure Provers = TheoryDataFun
 (

             Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))
         val _ = SimpleThread.fork true (fn () =>
           let
             val _ = register birthtime deadtime (Thread.self (), desc)
             val result =
-              let val (success, message, _, _, _) =
+              let val (success, (message, _), _, _, _) =
                 prover (get_timeout ()) NONE NONE name i (Proof.get_goal proof_state)
               in (success, message) end
               handle ResHolClause.TOO_TRIVIAL
                 => (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
               | ERROR msg