1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 10:14:18 2014 +0100
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 10:14:18 2014 +0100
1.3 @@ -19,7 +19,8 @@
1.4
1.5 val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context
1.6 val preplay_isar_step : Proof.context -> Time.time -> proof_method -> isar_step -> play_outcome
1.7 - val set_preplay_outcomes_of_isar_step : isar_preplay_data Unsynchronized.ref -> label ->
1.8 + val set_preplay_outcomes_of_isar_step : Proof.context -> Time.time ->
1.9 + isar_preplay_data Unsynchronized.ref -> isar_step ->
1.10 (proof_method * play_outcome Lazy.lazy) list -> unit
1.11 val preplay_outcome_of_isar_step : isar_preplay_data -> label -> proof_method ->
1.12 play_outcome Lazy.lazy
1.13 @@ -167,9 +168,17 @@
1.14 | add_preplay_outcomes play1 play2 =
1.15 Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2)))
1.16
1.17 -fun set_preplay_outcomes_of_isar_step preplay_data l meths_outcomes =
1.18 - preplay_data := Canonical_Label_Tab.map_default (l, [])
1.19 - (fold (AList.update (op =)) meths_outcomes) (!preplay_data)
1.20 +fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data
1.21 + (step as Prove (_, _, l, _, _, (_, meths))) meths_outcomes0 =
1.22 + let
1.23 + fun preplay meth = Lazy.lazy (fn () => preplay_isar_step ctxt timeout meth step)
1.24 + val meths_outcomes =
1.25 + fold (fn meth => AList.default (op =) (meth, preplay meth)) meths meths_outcomes0
1.26 + in
1.27 + preplay_data := Canonical_Label_Tab.map_default (l, [])
1.28 + (fold (AList.update (op =)) meths_outcomes) (!preplay_data)
1.29 + end
1.30 + | set_preplay_outcomes_of_isar_step _ _ _ _ _ = ()
1.31
1.32 fun preplay_outcome_of_isar_step preplay_data l meth =
1.33 (case Canonical_Label_Tab.lookup preplay_data l of