diff -r 0e17e92248ac -r 3c2dbd2e221f src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Tue Feb 04 23:11:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Tue Feb 04 23:11:18 2014 +0100
@@ -133,8 +133,8 @@
 
     val play_outcome = take_time timeout prove ()
   in
-    (if Config.get ctxt trace then preplay_trace ctxt assmsp goal play_outcome else ();
-     play_outcome)
+    if Config.get ctxt trace then preplay_trace ctxt assmsp goal play_outcome else ();
+    play_outcome
   end
 
 fun preplay_isar_step_for_method ctxt timeout meth =
@@ -200,7 +200,8 @@
   end
 
 fun preplay_outcome_of_isar_step_for_method preplay_data l =
-  the o AList.lookup (op =) (the (Canonical_Label_Tab.lookup preplay_data l))
+  AList.lookup (op =) (the (Canonical_Label_Tab.lookup preplay_data l))
+  #> the_default (Lazy.value Not_Played)
 
 fun fastest_method_of_isar_step preplay_data =
   the o Canonical_Label_Tab.lookup preplay_data