tuning

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu Dec 19 19:37:43 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu Dec 19 20:07:06 2013 +0100
@@ -18,7 +18,7 @@
     {get_preplay_outcome: label -> play_outcome,
      set_preplay_outcome: label -> play_outcome -> unit,
      preplay_quietly: Time.time -> isar_step -> play_outcome,
-     overall_preplay_stats: isar_proof -> play_outcome}
+     overall_preplay_outcome: isar_proof -> play_outcome}
 
   val proof_preplay_interface: bool -> Proof.context -> string -> string -> bool -> Time.time ->
     isar_proof -> preplay_interface
@@ -151,7 +151,7 @@
   {get_preplay_outcome: label -> play_outcome,
    set_preplay_outcome: label -> play_outcome -> unit,
    preplay_quietly: Time.time -> isar_step -> play_outcome,
-   overall_preplay_stats: isar_proof -> play_outcome}
+   overall_preplay_outcome: isar_proof -> play_outcome}
 
 fun enrich_context_with_local_facts proof ctxt =
   let
@@ -173,7 +173,8 @@
 
 fun merge_preplay_outcomes _ Play_Failed = Play_Failed
   | merge_preplay_outcomes Play_Failed _ = Play_Failed
-  | merge_preplay_outcomes (Play_Timed_Out t1) (Play_Timed_Out t2) = Play_Timed_Out (Time.+ (t1, t2))
+  | merge_preplay_outcomes (Play_Timed_Out t1) (Play_Timed_Out t2) =
+    Play_Timed_Out (Time.+ (t1, t2))
   | merge_preplay_outcomes (Played t1) (Play_Timed_Out t2) = Play_Timed_Out (Time.+ (t1, t2))
   | merge_preplay_outcomes (Play_Timed_Out t1) (Played t2) = Play_Timed_Out (Time.+ (t1, t2))
   | merge_preplay_outcomes (Played t1) (Played t2) = Played (Time.+ (t1, t2))
@@ -190,7 +191,7 @@
     {get_preplay_outcome = K (Played Time.zeroTime),
      set_preplay_outcome = K (K ()),
      preplay_quietly = K (K (Played Time.zeroTime)),
-     overall_preplay_stats = K (Played Time.zeroTime)} : preplay_interface
+     overall_preplay_outcome = K (Played Time.zeroTime)} : preplay_interface
   else
     let
       val ctxt = enrich_context_with_local_facts proof ctxt
@@ -215,10 +216,10 @@
         let
           fun add_step_to_tab step tab =
             (case label_of_step step of
-               NONE => tab
-             | SOME l =>
-               Canonical_Lbl_Tab.update_new
-                 (l, (fn () => preplay false preplay_timeout step) |> Lazy.lazy) tab)
+              NONE => tab
+            | SOME l =>
+              Canonical_Lbl_Tab.update_new
+                (l, (fn () => preplay false preplay_timeout step) |> Lazy.lazy) tab)
             handle Canonical_Lbl_Tab.DUP _ => raise Fail "Sledgehammer_Preplay: preplay time table"
         in
           Canonical_Lbl_Tab.empty
@@ -237,13 +238,13 @@
         try (label_of_step #> the #> get_preplay_outcome)
         #> the_default (Played Time.zeroTime)
 
-      fun overall_preplay_stats (Proof (_, _, steps)) =
+      fun overall_preplay_outcome (Proof (_, _, steps)) =
         fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime)
     in
       {get_preplay_outcome = get_preplay_outcome,
        set_preplay_outcome = set_preplay_outcome,
        preplay_quietly = preplay_quietly,
-       overall_preplay_stats = overall_preplay_stats}
+       overall_preplay_outcome = overall_preplay_outcome}
     end
 
 end;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Dec 19 19:37:43 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Dec 19 20:07:06 2013 +0100
@@ -342,7 +342,7 @@
         and isar_proof outer fix assms lems infs =
           Proof (fix, assms, lems @ isar_steps outer NONE [] infs)
 
-        val (preplay_interface as {overall_preplay_stats, ...}, isar_proof) =
+        val (preplay_interface as {overall_preplay_outcome, ...}, isar_proof) =
           refute_graph
 (*
           |> tap (tracing o prefix "Refute graph: " o string_of_refute_graph)
@@ -363,7 +363,7 @@
                preplay_interface
           |> isar_try0 ? try0 preplay_timeout preplay_interface
           |> postprocess_remove_unreferenced_steps (isar_try0 ? min_deps_of_step preplay_interface)
-          |> `overall_preplay_stats
+          |> `overall_preplay_outcome
           ||> (chain_direct_proof #> kill_useless_labels_in_proof #> relabel_proof)
 
         val isar_text =