1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Dec 04 18:23:50 2012 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Dec 04 19:09:44 2012 +0100
     1.3 @@ -361,19 +361,24 @@
     1.4  
     1.5  fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ())
     1.6  
     1.7 -
     1.8 -fun get_prover ctxt args =
     1.9 +fun get_prover_name ctxt args =
    1.10    let
    1.11      fun default_prover_name () =
    1.12        hd (#provers (Sledgehammer_Isar.default_params ctxt []))
    1.13        handle List.Empty => error "No ATP available."
    1.14 -    fun get_prover name =
    1.15 -      (name, Sledgehammer_Minimize.get_minimizing_prover ctxt
    1.16 -                Sledgehammer_Provers.Normal (K (K ())) name)
    1.17    in
    1.18      (case AList.lookup (op =) args proverK of
    1.19 -      SOME name => get_prover name
    1.20 -    | NONE => get_prover (default_prover_name ()))
    1.21 +      SOME name => name
    1.22 +    | NONE => default_prover_name ())
    1.23 +  end
    1.24 +
    1.25 +fun get_prover ctxt name params goal all_facts =
    1.26 +  let
    1.27 +    fun learn prover =
    1.28 +      Sledgehammer_MaSh.mash_learn_proof ctxt params prover (prop_of goal) all_facts
    1.29 +  in
    1.30 +    Sledgehammer_Minimize.get_minimizing_prover ctxt Sledgehammer_Provers.Normal
    1.31 +      learn name
    1.32    end
    1.33  
    1.34  type stature = ATP_Problem_Generate.stature
    1.35 @@ -401,7 +406,7 @@
    1.36    SH_FAIL of int * int |
    1.37    SH_ERROR
    1.38  
    1.39 -fun run_sh prover_name prover fact_filter type_enc strict max_facts slice
    1.40 +fun run_sh prover_name fact_filter type_enc strict max_facts slice
    1.41        lam_trans uncurried_aliases e_selection_heuristic term_order force_sos
    1.42        hard_timeout timeout preplay_timeout sh_minimizeLST
    1.43        max_new_mono_instancesLST max_mono_itersLST dir pos st =
    1.44 @@ -472,6 +477,7 @@
    1.45            |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name
    1.46                   (the_default default_max_facts max_facts)
    1.47                   Sledgehammer_Fact.no_fact_override hyp_ts concl_t
    1.48 +        val prover = get_prover ctxt prover_name params goal facts
    1.49          val problem =
    1.50            {state = st', goal = goal, subgoal = i,
    1.51             subgoal_count = Sledgehammer_Util.subgoal_count st,
    1.52 @@ -494,10 +500,11 @@
    1.53  fun run_sledgehammer trivial args reconstructor named_thms id
    1.54        ({pre=st, log, pos, ...}: Mirabelle.run_args) =
    1.55    let
    1.56 +    val ctxt = Proof.context_of st
    1.57      val triv_str = if trivial then "[T] " else ""
    1.58      val _ = change_data id inc_sh_calls
    1.59      val _ = if trivial then () else change_data id inc_sh_nontriv_calls
    1.60 -    val (prover_name, prover) = get_prover (Proof.context_of st) args
    1.61 +    val prover_name = get_prover_name ctxt args
    1.62      val fact_filter = AList.lookup (op =) args fact_filterK |> the_default fact_filter_default
    1.63      val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default
    1.64      val strict = AList.lookup (op =) args strictK |> the_default strict_default
    1.65 @@ -526,8 +533,8 @@
    1.66      val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK
    1.67      val hard_timeout = SOME (4 * timeout)
    1.68      val (msg, result) =
    1.69 -      run_sh prover_name prover fact_filter type_enc strict max_facts slice
    1.70 -        lam_trans uncurried_aliases e_selection_heuristic term_order force_sos
    1.71 +      run_sh prover_name fact_filter type_enc strict max_facts slice lam_trans
    1.72 +        uncurried_aliases e_selection_heuristic term_order force_sos
    1.73          hard_timeout timeout preplay_timeout sh_minimizeLST
    1.74          max_new_mono_instancesLST max_mono_itersLST dir pos st
    1.75    in
    1.76 @@ -565,7 +572,7 @@
    1.77    let
    1.78      val ctxt = Proof.context_of st
    1.79      val n0 = length (these (!named_thms))
    1.80 -    val (prover_name, _) = get_prover ctxt args
    1.81 +    val prover_name = get_prover_name ctxt args
    1.82      val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default
    1.83      val strict = AList.lookup (op =) args strictK |> the_default strict_default
    1.84      val timeout =