1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Oct 26 17:35:54 2010 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Oct 26 20:09:38 2010 +0200
     1.3 @@ -316,10 +316,11 @@
     1.4  
     1.5  fun get_prover ctxt args =
     1.6    let
     1.7 +    val thy = ProofContext.theory_of ctxt
     1.8      fun default_prover_name () =
     1.9        hd (#provers (Sledgehammer_Isar.default_params ctxt []))
    1.10        handle Empty => error "No ATP available."
    1.11 -    fun get_prover name = (name, Sledgehammer.get_prover ctxt false name)
    1.12 +    fun get_prover name = (name, Sledgehammer.get_prover thy false name)
    1.13    in
    1.14      (case AList.lookup (op =) args proverK of
    1.15        SOME name => get_prover name

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Oct 26 17:35:54 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Oct 26 20:09:38 2010 +0200
     2.3 @@ -63,7 +63,7 @@
     2.4    val kill_provers : unit -> unit
     2.5    val running_provers : unit -> unit
     2.6    val messages : int option -> unit
     2.7 -  val get_prover : Proof.context -> bool -> string -> prover
     2.8 +  val get_prover : theory -> bool -> string -> prover
     2.9    val run_sledgehammer :
    2.10      params -> bool -> int -> relevance_override -> (string -> minimize_command)
    2.11      -> Proof.state -> bool * Proof.state
    2.12 @@ -410,14 +410,13 @@
    2.13    | failure_from_smt_failure (SMT_Solver.Counterexample _) = Unprovable
    2.14    | failure_from_smt_failure (SMT_Solver.Other_Failure _) = UnknownError
    2.15  
    2.16 -fun run_smt_solver ctxt remote ({timeout, ...} : params) minimize_command
    2.17 +fun run_smt_solver remote ({timeout, ...} : params) minimize_command
    2.18                     ({state, subgoal, subgoal_count, axioms, ...}
    2.19                      : prover_problem) =
    2.20    let
    2.21      val {outcome, used_facts, run_time_in_msecs} =
    2.22        SMT_Solver.smt_filter remote timeout state
    2.23                              (map_filter (try dest_Untranslated) axioms) subgoal
    2.24 -    val outcome' = outcome |> Option.map failure_from_smt_failure (* FIXME *)
    2.25      val message =
    2.26        case outcome of
    2.27          NONE =>
    2.28 @@ -425,22 +424,18 @@
    2.29                           (apply_on_subgoal subgoal subgoal_count ^
    2.30                            command_call smtN (map fst used_facts)) ^
    2.31          minimize_line minimize_command (map fst used_facts)
    2.32 -      | SOME (failure as SMT_Solver.Other_Failure _) =>
    2.33 -        SMT_Solver.string_of_failure ctxt
    2.34 -          (SMT_Solver.solver_name_of (Context.Proof ctxt)) failure
    2.35 -      | SOME _ => string_for_failure (the outcome')
    2.36 +      | SOME SMT_Solver.Time_Out => "Timed out."
    2.37 +      | SOME (SMT_Solver.Counterexample _) => "The SMT problem is unprovable."
    2.38 +      | SOME (failure as SMT_Solver.Other_Failure message) => message
    2.39 +    val outcome = outcome |> Option.map failure_from_smt_failure (* FIXME *)
    2.40    in
    2.41 -    {outcome = outcome', used_axioms = used_facts,
    2.42 -     run_time_in_msecs = run_time_in_msecs, message = message}
    2.43 +    {outcome = outcome, used_axioms = used_facts,
    2.44 +     run_time_in_msecs = SOME run_time_in_msecs, message = message}
    2.45    end
    2.46  
    2.47 -fun get_prover ctxt auto name =
    2.48 -  let val thy = ProofContext.theory_of ctxt in
    2.49 -    if is_smt_prover name then
    2.50 -      run_smt_solver ctxt (String.isPrefix remote_prefix name)
    2.51 -    else
    2.52 -      run_atp auto name (get_atp thy name)
    2.53 -  end
    2.54 +fun get_prover thy auto name =
    2.55 +  if is_smt_prover name then run_smt_solver (String.isPrefix remote_prefix name)
    2.56 +  else run_atp auto name (get_atp thy name)
    2.57  
    2.58  fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
    2.59                 auto minimize_command
    2.60 @@ -459,7 +454,7 @@
    2.61      fun go () =
    2.62        let
    2.63          fun really_go () =
    2.64 -          get_prover ctxt auto name params (minimize_command name) problem
    2.65 +          get_prover thy auto name params (minimize_command name) problem
    2.66            |> (fn {outcome, message, ...} =>
    2.67                   (if is_some outcome then "none" else "some", message))
    2.68          val (outcome_code, message) =
    2.69 @@ -508,7 +503,8 @@
    2.70      let
    2.71        val _ = Proof.assert_backward state
    2.72        val thy = Proof.theory_of state
    2.73 -      val {context = ctxt, facts = chained_ths, goal} = Proof.goal state
    2.74 +      val ctxt = Proof.context_of state
    2.75 +      val {facts = chained_ths, goal, ...} = Proof.goal state
    2.76        val (_, hyp_ts, concl_t) = strip_subgoal goal i
    2.77        val _ = () |> not blocking ? kill_provers
    2.78        val _ = if auto then () else Output.urgent_message "Sledgehammering..."

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Oct 26 17:35:54 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Oct 26 20:09:38 2010 +0200
     3.3 @@ -92,8 +92,7 @@
     3.4                     state axioms =
     3.5    let
     3.6      val thy = Proof.theory_of state
     3.7 -    val ctxt = Proof.context_of state
     3.8 -    val prover = get_prover ctxt false prover_name
     3.9 +    val prover = get_prover thy false prover_name
    3.10      val msecs = Time.toMilliseconds timeout
    3.11      val _ = Output.urgent_message ("Sledgehammer minimize: " ^ quote prover_name ^ ".")
    3.12      val {goal, ...} = Proof.goal state