src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML

   type label = Sledgehammer_Isar_Proof.label
 
   val trace : bool Config.T
 
   type isar_preplay_data =
-    {preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
+    {reset_preplay_outcomes: isar_step -> unit,
      set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
+     preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
      preplay_quietly: Time.time -> isar_step -> play_outcome,
      overall_preplay_outcome: isar_proof -> play_outcome}
 
   val preplay_data_of_isar_proof : bool -> Proof.context -> string -> string -> bool -> Time.time ->
     isar_proof -> isar_preplay_data

       (if Config.get ctxt trace then preplay_trace ctxt facts goal play_outcome else ();
        play_outcome)
     end
 
 type isar_preplay_data =
-  {preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
+  {reset_preplay_outcomes: isar_step -> unit,
    set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
+   preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
    preplay_quietly: Time.time -> isar_step -> play_outcome,
    overall_preplay_outcome: isar_proof -> play_outcome}
 
 fun enrich_context_with_local_facts proof ctxt =
   let

    Precondition: The proof must be labeled canonically; cf.
    "Slegehammer_Isar_Proof.relabel_isar_proof_canonically". *)
 fun preplay_data_of_isar_proof debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
   if not do_preplay then
     (* the "dont_preplay" option pretends that everything works just fine *)
-    {preplay_outcome = K (K (Lazy.value (Played Time.zeroTime))),
+    {reset_preplay_outcomes = K (),
      set_preplay_outcome = K (K (K ())),
+     preplay_outcome = K (K (Lazy.value (Played Time.zeroTime))),
      preplay_quietly = K (K (Played Time.zeroTime)),
      overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data
   else
     let
       val ctxt = enrich_context_with_local_facts proof ctxt

       (* preplay steps treating exceptions like timeouts *)
       fun preplay_quietly timeout (step as Prove (_, _, _, _, _, (_, (meth :: _) :: _))) =
           preplay true timeout meth step
         | preplay_quietly _ _ = Played Time.zeroTime
 
-      fun add_step_to_tab (step as Prove (_, _, l, _, _, (_, methss))) =
-          Canonical_Label_Tab.update_new
-            (l, maps (map (fn meth =>
-               (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step)))) methss)
-        | add_step_to_tab _ = I
-
-      val preplay_tab =
-        Canonical_Label_Tab.empty
-        |> fold_isar_steps add_step_to_tab (steps_of_proof proof)
-        |> Unsynchronized.ref
+      val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty
+
+      fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, methss))) =
+          preplay_tab := Canonical_Label_Tab.update (l, maps (map (fn meth =>
+              (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step)))) methss)
+            (!preplay_tab)
+        | reset_preplay_outcomes _ = ()
+
+      fun set_preplay_outcome l meth result =
+        preplay_tab := Canonical_Label_Tab.map_entry l
+          (AList.update (op =) (meth, Lazy.value result)) (!preplay_tab)
 
       fun preplay_outcome l meth =
         (case Canonical_Label_Tab.lookup (!preplay_tab) l of
           SOME meths_outcomes =>
           (case AList.lookup (op =) meths_outcomes meth of
             SOME outcome => outcome
           | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method")
         | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label")
 
-      fun set_preplay_outcome l meth result =
-        preplay_tab := Canonical_Label_Tab.map_entry l
-          (AList.update (op =) (meth, Lazy.value result)) (!preplay_tab)
+      val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) ()
 
       fun result_of_step (Prove (_, _, l, _, _, (_, (meth :: _) :: _))) =
           Lazy.force (preplay_outcome l meth)
         | result_of_step _ = Played Time.zeroTime
 
       fun overall_preplay_outcome (Proof (_, _, steps)) =
         fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime)
     in
-      {preplay_outcome = preplay_outcome,
+      {reset_preplay_outcomes = reset_preplay_outcomes,
        set_preplay_outcome = set_preplay_outcome,
+       preplay_outcome = preplay_outcome,
        preplay_quietly = preplay_quietly,
        overall_preplay_outcome = overall_preplay_outcome}
     end
 
 end;