src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Fri Jan 31 19:16:41 2014 +0100
@@ -31,10 +31,10 @@
 fun try0_step _ _ (step as Let _) = step
   | try0_step preplay_timeout
       ({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data)
-      (step as Prove (_, _, l, _, _, _)) =
+      (step as Prove (_, _, l, _, _, (_, (meth :: _) :: _))) =
     let
       val timeout =
-        (case preplay_outcome l of
+        (case Lazy.force (preplay_outcome l meth) of
           Played time => Time.+ (time, slack)
         | _ => preplay_timeout)
 
@@ -44,7 +44,8 @@
         | _ => NONE)
     in
       (case Par_List.get_some try_variant (variants_of_step step) of
-        SOME (step', result) => (set_preplay_outcome l result; step')
+        SOME (step' as Prove (_, _, _, _, _, (_, (meth' :: _) :: _)), result) =>
+        (set_preplay_outcome l meth' result; step')
       | NONE => step)
     end