# HG changeset patch
# User blanchet
# Date 1387472841 -3600
# Node ID 037046aab457ab05be3d119703bed035591a9801
# Parent  4e58a38b330ba9023bb57f3209bda66b9873f63b
tuning

diff -r 4e58a38b330b -r 037046aab457 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu Dec 19 17:52:58 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu Dec 19 18:07:21 2013 +0100
@@ -42,7 +42,7 @@
 
 datatype preplay_result =
   Preplay_Success of bool * Time.time |
-  Preplay_Failure of exn
+  Preplay_Failure
 
 val zero_preplay_time = (false, Time.zeroTime) (* 0 ms *)
 val some_preplay_time = (true, Time.zeroTime)  (* > 0 ms *)
@@ -214,18 +214,19 @@
         handle exn =>
                if Exn.is_interrupt exn then
                  reraise exn
-               else if not quietly andalso debug then
-                 (warning ("Preplay failure:\n  " ^ @{make_string} step ^ "\n  " ^
-                    @{make_string} exn);
-                  Preplay_Failure exn)
                else
-                 Preplay_Failure exn
+                (if not quietly andalso debug then
+                   warning ("Preplay failure:\n  " ^ @{make_string} step ^ "\n  " ^
+                     @{make_string} exn)
+                 else
+                   ();
+                 Preplay_Failure)
 
       (* preplay steps treating exceptions like timeouts *)
       fun preplay_quietly timeout step =
         (case preplay true timeout step of
           Preplay_Success preplay_time => preplay_time
-        | Preplay_Failure _ => (true, timeout))
+        | Preplay_Failure => (true, timeout))
 
       val preplay_tab =
         let
@@ -252,7 +253,7 @@
       fun get_preplay_time l =
         (case get_preplay_result l of
           Preplay_Success preplay_time => preplay_time
-        | Preplay_Failure _ => some_preplay_time)
+        | Preplay_Failure => some_preplay_time)
 
       fun set_preplay_time l = set_preplay_result l o Preplay_Success
 
@@ -263,7 +264,7 @@
       fun do_step step =
         (case result_of_step step of
           Preplay_Success preplay_time => apfst (add_preplay_time preplay_time)
-        | Preplay_Failure _ => apsnd (K true))
+        | Preplay_Failure => apsnd (K true))
 
       fun overall_preplay_stats (Proof (_, _, steps)) =
         fold_isar_steps do_step steps (zero_preplay_time, false)