--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Sun Feb 02 20:53:51 2014 +0100
@@ -30,7 +30,7 @@
fun try0_step _ _ (step as Let _) = step
| try0_step preplay_timeout
- ({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data)
+ ({preplay_outcome, set_preplay_outcomes, preplay_quietly, ...} : isar_preplay_data)
(step as Prove (_, _, l, _, _, (_, meth :: _))) =
let
val timeout =
@@ -45,8 +45,8 @@
in
(* FIXME: create variant after success *)
(case Par_List.get_some try_variant (variants_of_step step) of
- SOME (step' as Prove (_, _, _, _, _, (_, meth' :: _)), result) =>
- (set_preplay_outcome l meth' result; step')
+ SOME (step' as Prove (_, _, _, _, _, (_, meth' :: _)), outcome) =>
+ (set_preplay_outcomes l [(meth', Lazy.value outcome)]; step')
| NONE => step)
end