# HG changeset patch
# User blanchet
# Date 1391434216 -3600
# Node ID b90c06d54d38640497f455be2a3605d8ee8262e2
# Parent  d4a033f07800083af29620812aa2d15e1a243125
when merging, don't try methods that failed or timed out for either of the steps for the combined step

diff -r d4a033f07800 -r b90c06d54d38 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 13:37:23 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 14:30:16 2014 +0100
@@ -80,9 +80,20 @@
     | _ => raise Fail "Sledgehammer_Isar_Compress: update_steps")
   end
 
-fun try_merge (Prove (_, [], l1, _, [], (lfs1, gfs1), meths1))
+fun merge_methods preplay_data (l1, meths1) (l2, meths2) =
+  let
+    fun is_method_hopeful l meth =
+      let val outcome = preplay_outcome_of_isar_step_for_method preplay_data l meth in
+        not (Lazy.is_finished outcome) orelse
+        (case Lazy.force outcome of Played _ => true | _ => false)
+      end
+  in
+    inter (op =) (filter (is_method_hopeful l1) meths1) (filter (is_method_hopeful l2) meths2)
+  end
+
+fun try_merge preplay_data (Prove (_, [], l1, _, [], (lfs1, gfs1), meths1))
       (Prove (qs2, fix, l2, t, subproofs, (lfs2, gfs2), meths2)) =
-    (case inter (op =) meths1 meths2 of
+    (case merge_methods preplay_data (l1, meths1) (l2, meths2) of
       [] => NONE
     | meths =>
       let
@@ -91,7 +102,7 @@
       in
         SOME (Prove (qs2, fix, l2, t, subproofs, (lfs, gfs), meths))
       end)
-  | try_merge _ _ = NONE
+  | try_merge _ _ _ = NONE
 
 val compress_degree = 2
 val merge_timeout_slack_time = seconds 0.005
@@ -163,7 +174,7 @@
               val subs'' = subs @ nontriv_subs
               val lfs'' = union (op =) lfs (subtract (op =) (map fst assms) lfs')
               val gfs'' = union (op =) gfs' gfs
-              val meths'' as _ :: _ = inter (op =) meths' meths
+              val meths'' as _ :: _ = merge_methods (!preplay_data) (l', meths') (l, meths)
               val step'' = Prove (qs, fix, l, t, subs'', (lfs'', gfs''), meths'')
 
               (* check if the modified step can be preplayed fast enough *)
@@ -224,7 +235,7 @@
               (* only touch steps that can be preplayed successfully *)
               val Played time = forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l
 
-              val succs' = map (try_merge cand #> the) succs
+              val succs' = map (try_merge (!preplay_data) cand #> the) succs
 
               val times0 = map ((fn Played time => time) o
                 forced_intermediate_preplay_outcome_of_isar_step (!preplay_data)) labels