--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Thu Dec 19 17:11:54 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Thu Dec 19 17:24:17 2013 +0100
@@ -88,8 +88,8 @@
val (failed, reconstr, ext_time) =
(case preplay of
Played (reconstr, time) => (false, reconstr, (SOME (false, time)))
- | Play_Timed_Out (reconstr, time) =>
- (false, reconstr, if time = Time.zeroTime then NONE else SOME (true, time))
+ | Not_Played reconstr => (false, reconstr, NONE)
+ | Play_Timed_Out (reconstr, time) => (false, reconstr, SOME (true, time))
| Play_Failed reconstr => (true, reconstr, NONE))
val try_line =
([], map fst extra)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 19 17:11:54 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 19 17:24:17 2013 +0100
@@ -404,7 +404,7 @@
else List.last reconstrs
in
if timeout = Time.zeroTime then
- Play_Timed_Out (get_preferred reconstrs, Time.zeroTime)
+ Not_Played (get_preferred reconstrs)
else
let
val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Dec 19 17:11:54 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Dec 19 17:24:17 2013 +0100
@@ -405,7 +405,8 @@
fun isar_proof_would_be_a_good_idea preplay =
(case preplay of
Played (reconstr, _) => reconstr = SMT
- | Play_Timed_Out _ => false
+ | Not_Played _ => false
+ | Play_Timed_Out _ => true
| Play_Failed _ => true)
fun proof_text ctxt isar_proofs isar_params num_chained
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Thu Dec 19 17:11:54 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Thu Dec 19 17:24:17 2013 +0100
@@ -15,6 +15,7 @@
datatype play =
Played of reconstructor * Time.time |
+ Not_Played of reconstructor |
Play_Timed_Out of reconstructor * Time.time |
Play_Failed of reconstructor
@@ -35,6 +36,7 @@
datatype play =
Played of reconstructor * Time.time |
+ Not_Played of reconstructor |
Play_Timed_Out of reconstructor * Time.time |
Play_Failed of reconstructor