val get_prover: theory -> string -> ATP_Wrapper.prover option

   val get_prover: theory -> string -> ATP_Wrapper.prover option

   val print_provers: theory -> unit

   val print_provers: theory -> unit

   val sledgehammer: string list -> Proof.state -> unit

   val sledgehammer: string list -> Proof.state -> unit

 end;

 end;

 struct

 struct

 (** preferences **)

 (** preferences **)

 val message_store_limit = 20;

 val message_store_limit = 20;

         val _ = Toplevel.thread true (fn () =>

         val _ = Toplevel.thread true (fn () =>

           let

           let

             val _ = register birth_time death_time (Thread.self (), desc);

             val _ = register birth_time death_time (Thread.self (), desc);

             val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal));

             val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal));

             val message = #message (prover (! timeout) problem)

             val message = #message (prover (! timeout) problem)

                   "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"

                   "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"

                 | ERROR msg => ("Error: " ^ msg);

                 | ERROR msg => ("Error: " ^ msg);

             val _ = unregister message (Thread.self ());

             val _ = unregister message (Thread.self ());

           in () end);

           in () end);

       in () end);

       in () end);