src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML

 open Sledgehammer_Isar_Proof
 open Sledgehammer_Isar_Preplay
 
 val dummy_isar_step = Let (Term.dummy, Term.dummy)
 
-(* traverses steps in post-order and collects the steps with the given labels *)
 fun collect_successors steps lbls =
   let
     fun collect_steps _ ([], accu) = ([], accu)
       | collect_steps [] accum = accum
       | collect_steps (step :: steps) accum = collect_steps steps (collect_step step accum)

         | accum => collect_subproofs subproofs accum)
   in
     rev (snd (collect_steps steps (lbls, [])))
   end
 
-(* traverses steps in reverse post-order and inserts the given updates *)
 fun update_steps steps updates =
   let
     fun update_steps [] updates = ([], updates)
       | update_steps steps [] = (steps, [])
       | update_steps (step :: steps) updates = update_step step (update_steps steps updates)

         not (Lazy.is_finished outcome) orelse
         (case Lazy.force outcome of Played _ => true | _ => false)
       end
   in
     meths2 @ subtract (op =) meths2 meths1
-    |> filter (is_method_hopeful l1 andf is_method_hopeful l2)
+    |> List.partition (is_method_hopeful l1 andf is_method_hopeful l2)
+    |> op @
   end
 
 fun try_merge preplay_data (Prove (_, [], l1, _, subproofs1, (lfs1, gfs1), meths1, comment1))
       (Prove (qs2, fix, l2, t, subproofs2, (lfs2, gfs2), meths2, comment2)) =
     (case merge_methods preplay_data (l1, meths1) (l2, meths2) of

       end)
   | try_merge _ _ _ = NONE
 
 val compress_degree = 2
 val merge_timeout_slack_time = seconds 0.005
-val merge_timeout_slack_factor = 1.25
+val merge_timeout_slack_factor = 1.5
 
 fun slackify_merge_timeout time =
   time_mult merge_timeout_slack_factor (Time.+ (merge_timeout_slack_time, time))
 
 (* Precondition: The proof must be labeled canonically. *)

         let
           (* (#successors, (size_of_term t, position)) *)
           fun cand_key (i, l, t_size) = (length (get_successors l), (t_size, i))
 
           val compression_ord =
-            prod_ord int_ord (prod_ord (int_ord #> rev_order) int_ord)
-            #> rev_order
+            prod_ord int_ord (prod_ord (int_ord #> rev_order) int_ord) #> rev_order
 
           val cand_ord = pairself cand_key #> compression_ord
 
           fun pop_next_candidate [] = (NONE, [])
             | pop_next_candidate (cands as (cand :: cands')) =
-              let
-                val best as (i, _, _) =
-                  fold (fn x => fn y => if cand_ord (x, y) = GREATER then x else y) cands' cand
-              in (SOME best, filter_out (fn (j, _, _) => j = i) cands) end
+              fold (fn x => fn y => if cand_ord (x, y) = GREATER then x else y) cands' cand
+              |> (fn best => (SOME best, remove (op =) best cands))
 
           val candidates =
             let
               fun add_cand (i, Prove (_, _, l, t, _, _, _, _)) = cons (i, l, size_of_term t)
                 | add_cand _ = I
             in
-              (steps
-               |> split_last |> fst (* keep last step *)
-               |> fold_index add_cand) []
+              (* the very last step is not a candidate *)
+              (steps |> split_last |> fst |> fold_index add_cand) []
             end
 
           fun try_eliminate (i, l, _) labels steps =
             let
               val ((cand as Prove (_, _, _, _, _, (lfs, _), _, _)) :: steps') = drop i steps

             if not (compress_further ()) then
               steps
             else
               (case pop_next_candidate candidates of
                 (NONE, _) => steps (* no more candidates for elimination *)
-              | (SOME (cand as (_, l, _)), candidates) =>
+              | (SOME (cand as (i, l, _)), candidates') =>
                 let val successors = get_successors l in
                   if length successors > compress_degree then steps
-                  else compression_loop candidates (try_eliminate cand successors steps)
+                  else compression_loop candidates' (try_eliminate cand successors steps)
                 end)
         in
           compression_loop candidates steps
           |> remove (op =) dummy_isar_step
         end