# HG changeset patch
# User smolkas
# Date 1373631486 -7200
# Node ID 5445f1c53666d45d3bd2bec15ede6ee765573601
# Parent  32e7f3b7c53a1d71bc4f108aca9d967bec2cb028
more reasonable preplay_interface semantics

diff -r 32e7f3b7c53a -r 5445f1c53666 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Fri Jul 12 14:18:06 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Fri Jul 12 14:18:06 2013 +0200
@@ -225,15 +225,12 @@
 
       fun set_preplay_fail b = fail := b
 
-      fun preplay' timeout step =
-        (* after preplay has failed once, exact preplay times are pointless *)
-        if preplay_fail () then some_preplay_time
-          else preplay debug preplay_trace type_enc lam_trans ctxt timeout step
+      val preplay = preplay debug preplay_trace type_enc lam_trans ctxt
 
       (* preplay steps without registering preplay_fails, treating exceptions
          like timeouts *)
       fun preplay_quietly timeout step =
-        try (preplay' timeout) step
+        try (preplay timeout) step
         |> the_default (true, timeout)
 
       val preplay_time_tab =
@@ -243,7 +240,7 @@
               NONE => tab
             | SOME l =>
                 Canonical_Lbl_Tab.update_new
-                  (l, (fn () => preplay' preplay_timeout step) |> Lazy.lazy)
+                  (l, (fn () => preplay preplay_timeout step) |> Lazy.lazy)
                   tab
             handle Canonical_Lbl_Tab.DUP _ =>
               raise Fail "Sledgehammer_Preplay: preplay time table"