1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jul 18 08:44:04 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jul 18 08:44:04 2012 +0200
     1.3 @@ -86,7 +86,10 @@
     1.4                 |> take num_facts}
     1.5      fun really_go () =
     1.6        problem
     1.7 -      |> get_minimizing_prover ctxt mode name params minimize_command
     1.8 +      |> get_minimizing_prover ctxt mode
     1.9 +             (mash_learn_proof ctxt params (prop_of goal)
    1.10 +                               (map untranslated_fact facts))
    1.11 +             name params minimize_command
    1.12        |> (fn {outcome, preplay, message, message_tail, ...} =>
    1.13               (if outcome = SOME ATP_Proof.TimedOut then timeoutN
    1.14                else if is_some outcome then noneN