diff -r a368cd086e46 -r c8b04da1bd01 src/HOL/Tools/Sledgehammer/sledgehammer_print.ML
--- 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