src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Wed Jul 17 21:48:21 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Wed Jul 17 23:36:33 2013 +0200
@@ -284,6 +284,8 @@
             val succs = collect_successors steps' succ_lbls
             val succs' = map (try_merge cand #> the) succs
 
+            (* TODO: should be lazy: stop preplaying as soon as one step
+               fails/times out *)
             val preplay_times =
               map (uncurry preplay_quietly) (timeouts ~~ succs')