--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Wed Dec 18 22:55:43 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Thu Dec 19 09:28:20 2013 +0100
@@ -88,12 +88,12 @@
val (failed, reconstr, ext_time) =
case preplay of
Played (reconstr, time) => (false, reconstr, (SOME (false, time)))
- | Trust_Playable (reconstr, time) =>
+ | Play_Timed_Out (reconstr, time) =>
(false, reconstr,
(case time of
NONE => NONE
| SOME time => if time = Time.zeroTime then NONE else SOME (true, time)))
- | Failed_to_Play reconstr => (true, reconstr, NONE)
+ | Play_Failed reconstr => (true, reconstr, NONE)
val try_line =
([], map fst extra)
|> reconstructor_command reconstr subgoal subgoal_count (map fst chained) num_chained