1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 10:14:18 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 10:14:18 2014 +0100
     1.3 @@ -296,7 +296,7 @@
     1.4  
     1.5          fun str_of_meth l meth =
     1.6            string_of_proof_method meth ^ " " ^
     1.7 -          str_of_preplay_outcome (preplay_outcome_of_isar_step (!preplay_data) l meth)
     1.8 +          str_of_preplay_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)
     1.9          fun comment_of l = map (str_of_meth l) #> commas
    1.10  
    1.11          fun trace_isar_proof label proof =
    1.12 @@ -314,7 +314,8 @@
    1.13            |> try0_isar ? try0_isar_proof ctxt preplay_timeout preplay_data
    1.14            |> tap (trace_isar_proof "Tried0")
    1.15            |> postprocess_isar_proof_remove_unreferenced_steps
    1.16 -               (try0_isar ? minimize_isar_step_dependencies ctxt preplay_data)
    1.17 +               (keep_fastest_method_of_isar_step (!preplay_data)
    1.18 +                #> try0_isar(*### minimize*) ? minimize_isar_step_dependencies ctxt preplay_data)
    1.19            |> tap (trace_isar_proof "Minimized")
    1.20            |> `(preplay_outcome_of_isar_proof (!preplay_data))
    1.21            ||> chain_isar_proof