src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sun Feb 02 20:53:51 2014 +0100
@@ -16,8 +16,7 @@
   val trace : bool Config.T
 
   type isar_preplay_data =
-    {reset_preplay_outcomes: isar_step -> unit,
-     set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
+    {set_preplay_outcomes: label -> (proof_method * play_outcome Lazy.lazy) list -> 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}
@@ -136,8 +135,7 @@
     end
 
 type isar_preplay_data =
-  {reset_preplay_outcomes: isar_step -> unit,
-   set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
+  {set_preplay_outcomes: label -> (proof_method * play_outcome Lazy.lazy) list -> 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}
@@ -177,8 +175,7 @@
 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 *)
-    {reset_preplay_outcomes = K (),
-     set_preplay_outcome = K (K (K ())),
+    {set_preplay_outcomes = 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
@@ -205,15 +202,9 @@
 
       val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty
 
-      fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) =
-          preplay_tab := Canonical_Label_Tab.update (l, map (fn meth =>
-              (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step))) meths)
-            (!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 set_preplay_outcomes l meths_outcomes =
+        preplay_tab := Canonical_Label_Tab.map_entry l (fold (AList.update (op =)) meths_outcomes)
+          (!preplay_tab)
 
       fun preplay_outcome l meth =
         (case Canonical_Label_Tab.lookup (!preplay_tab) l of
@@ -223,17 +214,22 @@
           | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method")
         | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label")
 
-      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)
+
+      fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) =
+          preplay_tab := Canonical_Label_Tab.update (l, map (fn meth =>
+              (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step))) meths)
+            (!preplay_tab)
+        | reset_preplay_outcomes _ = ()
+
+      val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) ()
     in
-      {reset_preplay_outcomes = reset_preplay_outcomes,
-       set_preplay_outcome = set_preplay_outcome,
+      {set_preplay_outcomes = set_preplay_outcomes,
        preplay_outcome = preplay_outcome,
        preplay_quietly = preplay_quietly,
        overall_preplay_outcome = overall_preplay_outcome}