1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Feb 02 20:53:51 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Feb 02 20:53:51 2014 +0100
     1.3 @@ -307,12 +307,12 @@
     1.4          val (play_outcome, isar_proof) =
     1.5            canonical_isar_proof
     1.6            |> tap (trace_isar_proof "Original")
     1.7 -          |> compress_isar_proof compress_isar preplay_data
     1.8 +          |> compress_isar_proof preplay_ctxt compress_isar preplay_data
     1.9            |> tap (trace_isar_proof "Compressed")
    1.10 -          |> try0_isar ? try0_isar_proof preplay_timeout preplay_data
    1.11 +          |> try0_isar ? try0_isar_proof preplay_ctxt preplay_timeout preplay_data
    1.12            |> tap (trace_isar_proof "Tried0")
    1.13            |> postprocess_isar_proof_remove_unreferenced_steps
    1.14 -               (try0_isar ? minimize_isar_step_dependencies preplay_data)
    1.15 +               (try0_isar ? minimize_isar_step_dependencies preplay_ctxt preplay_data)
    1.16            |> tap (trace_isar_proof "Minimized")
    1.17            |> `overall_preplay_outcome
    1.18            ||> chain_isar_proof