--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 03 10:14:18 2014 +0100
@@ -156,8 +156,7 @@
try the_single sub_steps
(* only touch proofs that can be preplayed sucessfully *)
- val Played time' =
- Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l' meth')
+ val Played time' = forced_preplay_outcome_of_isar_step (!preplay_data) l'
(* merge steps *)
val subs'' = subs @ nontriv_subs
@@ -184,7 +183,7 @@
if subproofs = [] then
step
else
- (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
+ (case forced_preplay_outcome_of_isar_step (!preplay_data) l of
Played time => elim_one_subproof time qs fix l t lfs gfs meths subproofs []
| _ => step)
@@ -224,13 +223,12 @@
val succ_meths = map (hd o snd o the o byline_of_isar_step) succs
(* only touch steps that can be preplayed successfully *)
- val Played time =
- Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)
+ val Played time = forced_preplay_outcome_of_isar_step (!preplay_data) l
val succs' = map (try_merge cand #> the) succs
- val times0 = map2 ((fn Played time => time) o Lazy.force oo
- preplay_outcome_of_isar_step_for_method (!preplay_data)) labels succ_meths
+ val times0 = map ((fn Played time => time) o
+ forced_preplay_outcome_of_isar_step (!preplay_data)) labels
val time_slice = time_mult (1.0 / (Real.fromInt (length labels))) time
val timeouts = map (curry Time.+ time_slice #> time_mult merge_timeout_slack) times0