diff -r d6d084186df0 -r 371cdc675cf9 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 06 23:11:14 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 06 23:26:40 2011 +0200
@@ -428,7 +428,7 @@
 fun play_one_line_proof debug timeout ths state i reconstructors =
   let
     fun play [] [] = Failed_to_Play (hd reconstructors)
-      | play (timed_out :: _) [] = Trust_Playable (timed_out, SOME timeout)
+      | play timed_outs [] = Trust_Playable (List.last timed_outs, SOME timeout)
       | play timed_out (reconstructor :: reconstructors) =
         let val timer = Timer.startRealTimer () in
           case timed_reconstructor reconstructor debug timeout ths state i of