# HG changeset patch
# User blanchet
# Date 1391370831 -3600
# Node ID 4aa3e1c6222c5a15f78e4b85def0451b97238e60
# Parent  e9fba9767d9202be2ae84331b9f697f0be23c5d6
take intersection rather than union of methods when merging steps -- more efficient and natural

diff -r e9fba9767d92 -r 4aa3e1c6222c src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Sun Feb 02 20:53:51 2014 +0100
@@ -81,13 +81,15 @@
 
 fun try_merge (Prove (_, [], l1, _, [], ((lfs1, gfs1), meths1)))
       (Prove (qs2, fix, l2, t, subproofs, ((lfs2, gfs2), meths2))) =
-    let
-      val lfs = union (op =) lfs1 (remove (op =) l1 lfs2)
-      val gfs = union (op =) gfs1 gfs2
-      val meths = fold_rev (insert (op =)) meths1 meths2
-    in
-      SOME (Prove (qs2, fix, l2, t, subproofs, ((lfs, gfs), meths)))
-    end
+    (case inter (op =) meths1 meths2 of
+      [] => NONE
+    | meths =>
+      let
+        val lfs = union (op =) lfs1 (remove (op =) l1 lfs2)
+        val gfs = union (op =) gfs1 gfs2
+      in
+        SOME (Prove (qs2, fix, l2, t, subproofs, ((lfs, gfs), meths)))
+      end)
   | try_merge _ _ = NONE
 
 val compress_degree = 2
@@ -237,7 +239,7 @@
               val play_outcomes = map2 preplay_quietly timeouts succs'
 
               (* ensure none of the modified successors timed out *)
-              val true = List.all (fn Played _ => true) play_outcomes
+              val true = forall (fn Played _ => true) play_outcomes
 
               val (steps1, _ :: steps2) = chop i steps
               (* replace successors with their modified versions *)