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 @@ -135,10 +135,8 @@
     1.4          val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0
     1.5  
     1.6          val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
     1.7 -        val (_, ctxt) =
     1.8 -          params
     1.9 -          |> map (fn (s, T) => (Binding.name s, SOME T, NoSyn))
    1.10 -          |> (fn fixes => ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes)
    1.11 +        val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
    1.12 +        val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
    1.13  
    1.14          val do_preplay = preplay_timeout <> Time.zeroTime
    1.15          val try0_isar = try0_isar andalso do_preplay
    1.16 @@ -283,19 +281,14 @@
    1.17            |> postprocess_isar_proof_remove_unreferenced_steps I
    1.18            |> relabel_isar_proof_canonically
    1.19  
    1.20 -        val preplay_ctxt = ctxt
    1.21 +        val ctxt = ctxt
    1.22            |> enrich_context_with_local_facts canonical_isar_proof
    1.23            |> silence_reconstructors debug
    1.24  
    1.25          val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
    1.26  
    1.27 -        fun init_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) =
    1.28 -            set_preplay_outcomes_of_isar_step preplay_data l (map (fn meth => (meth,
    1.29 -                Lazy.lazy (fn () => preplay_isar_step preplay_ctxt preplay_timeout meth step)))
    1.30 -              meths)
    1.31 -          | init_preplay_outcomes _ = ()
    1.32 -
    1.33 -        val _ = fold_isar_steps (K o init_preplay_outcomes)
    1.34 +        val _ = fold_isar_steps (fn meth =>
    1.35 +            K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth []))
    1.36            (steps_of_isar_proof canonical_isar_proof) ()
    1.37  
    1.38          fun str_of_preplay_outcome outcome =
    1.39 @@ -316,12 +309,12 @@
    1.40          val (play_outcome, isar_proof) =
    1.41            canonical_isar_proof
    1.42            |> tap (trace_isar_proof "Original")
    1.43 -          |> compress_isar_proof preplay_ctxt compress_isar preplay_data
    1.44 +          |> compress_isar_proof ctxt compress_isar preplay_data
    1.45            |> tap (trace_isar_proof "Compressed")
    1.46 -          |> try0_isar ? try0_isar_proof preplay_ctxt preplay_timeout preplay_data
    1.47 +          |> try0_isar ? try0_isar_proof ctxt preplay_timeout preplay_data
    1.48            |> tap (trace_isar_proof "Tried0")
    1.49            |> postprocess_isar_proof_remove_unreferenced_steps
    1.50 -               (try0_isar ? minimize_isar_step_dependencies preplay_ctxt preplay_data)
    1.51 +               (try0_isar ? minimize_isar_step_dependencies ctxt preplay_data)
    1.52            |> tap (trace_isar_proof "Minimized")
    1.53            |> `(preplay_outcome_of_isar_proof (!preplay_data))
    1.54            ||> chain_isar_proof