1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Dec 03 18:27:21 2010 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Dec 03 18:29:14 2010 +0100
     1.3 @@ -130,39 +130,36 @@
     1.4    val extend = I
     1.5    fun merge p : T = AList.merge (op =) (K true) p)
     1.6  
     1.7 -fun remotify_prover_if_available_and_not_already_remote thy name =
     1.8 +fun remotify_prover_if_available_and_not_already_remote ctxt name =
     1.9    if String.isPrefix remote_prefix name then
    1.10      SOME name
    1.11    else
    1.12      let val remote_name = remote_prefix ^ name in
    1.13 -      if is_prover_available thy remote_name then SOME remote_name else NONE
    1.14 +      if is_prover_available ctxt remote_name then SOME remote_name else NONE
    1.15      end
    1.16  
    1.17  fun remotify_prover_if_not_installed ctxt name =
    1.18 -  let val thy = ProofContext.theory_of ctxt in
    1.19 -    if is_prover_available thy name andalso is_prover_installed ctxt name then
    1.20 -      SOME name
    1.21 -    else
    1.22 -      remotify_prover_if_available_and_not_already_remote thy name
    1.23 -  end
    1.24 +  if is_prover_available ctxt name andalso is_prover_installed ctxt name then
    1.25 +    SOME name
    1.26 +  else
    1.27 +    remotify_prover_if_available_and_not_already_remote ctxt name
    1.28  
    1.29  fun avoid_too_many_local_threads _ _ [] = []
    1.30 -  | avoid_too_many_local_threads thy 0 provers =
    1.31 -    map_filter (remotify_prover_if_available_and_not_already_remote thy) provers
    1.32 -  | avoid_too_many_local_threads thy n (prover :: provers) =
    1.33 +  | avoid_too_many_local_threads ctxt 0 provers =
    1.34 +    map_filter (remotify_prover_if_available_and_not_already_remote ctxt)
    1.35 +               provers
    1.36 +  | avoid_too_many_local_threads ctxt n (prover :: provers) =
    1.37      let val n = if String.isPrefix remote_prefix prover then n else n - 1 in
    1.38 -      prover :: avoid_too_many_local_threads thy n provers
    1.39 +      prover :: avoid_too_many_local_threads ctxt n provers
    1.40      end
    1.41  
    1.42  (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
    1.43     timeout, it makes sense to put SPASS first. *)
    1.44  fun default_provers_param_value ctxt =
    1.45 -  let val thy = ProofContext.theory_of ctxt in
    1.46 -    [spassN, eN, vampireN, sine_eN, smtN]
    1.47 -    |> map_filter (remotify_prover_if_not_installed ctxt)
    1.48 -    |> avoid_too_many_local_threads thy (Multithreading.max_threads_value ())
    1.49 -    |> space_implode " "
    1.50 -  end
    1.51 +  [spassN, eN, vampireN, sine_eN, SMT_Solver.solver_name_of ctxt]
    1.52 +  |> map_filter (remotify_prover_if_not_installed ctxt)
    1.53 +  |> avoid_too_many_local_threads ctxt (Multithreading.max_threads_value ())
    1.54 +  |> space_implode " "
    1.55  
    1.56  val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
    1.57  fun default_raw_params ctxt =
    1.58 @@ -270,7 +267,6 @@
    1.59  fun hammer_away override_params subcommand opt_i relevance_override state =
    1.60    let
    1.61      val ctxt = Proof.context_of state
    1.62 -    val thy = Proof.theory_of state
    1.63      val _ = app check_raw_param override_params
    1.64    in
    1.65      if subcommand = runN then
    1.66 @@ -286,7 +282,7 @@
    1.67      else if subcommand = messagesN then
    1.68        messages opt_i
    1.69      else if subcommand = available_proversN then
    1.70 -      available_provers thy
    1.71 +      available_provers ctxt
    1.72      else if subcommand = running_proversN then
    1.73        running_provers ()
    1.74      else if subcommand = kill_proversN then