# HG changeset patch
# User blanchet
# Date 1406897037 -7200
# Node ID e081db351356c969e87be08840d3509594ccd899
# Parent  c822c1c069f8ce3d6c4cf0341a1d7601a2b4c9bd
export ML function

diff -r c822c1c069f8 -r e081db351356 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -10,6 +10,8 @@
 sig
   type fact = Sledgehammer_Fact.fact
   type fact_override = Sledgehammer_Fact.fact_override
+  type proof_method = Sledgehammer_Proof_Methods.proof_method
+  type play_outcome = Sledgehammer_Proof_Methods.play_outcome
   type mode = Sledgehammer_Prover.mode
   type params = Sledgehammer_Prover.params
 
@@ -18,6 +20,8 @@
   val timeoutN : string
   val unknownN : string
 
+  val play_one_line_proof : Time.time -> (string * 'a) list -> Proof.state -> int ->
+    proof_method * proof_method list list -> (string * 'a) list * (proof_method * play_outcome)
   val string_of_factss : (string * fact list) list -> string
   val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override ->
     Proof.state -> bool * (string * Proof.state)
@@ -59,7 +63,7 @@
   (quote name,
    if verbose then " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts else "")
 
-fun play_one_line_proof mode timeout used_facts state i (preferred, methss as (meth :: _) :: _) =
+fun play_one_line_proof timeout used_facts state i (preferred, methss as (meth :: _) :: _) =
   let
     fun dont_know () =
       (used_facts,
@@ -70,7 +74,6 @@
       dont_know ()
     else
       let
-        val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()
         val fact_names = used_facts |> map fst |> sort string_ord
 
         val {context = ctxt, facts = chained, goal} = Proof.goal state
@@ -176,7 +179,7 @@
         (if outcome = SOME ATP_Proof.TimedOut then timeoutN
          else if is_some outcome then noneN
          else someN,
-         fn () => message (fn () => play_one_line_proof mode preplay_timeout used_facts state subgoal
+         fn () => message (fn () => play_one_line_proof preplay_timeout used_facts state subgoal
            preferred_methss)))
 
     fun go () =