src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML

       val step_vect = steps |> map SOME |> Vector.fromList
       val n_metis = add_metis_steps_top_level steps 0
       val target_n_metis = Real.fromInt n_metis / isar_compress |> Real.round
 
       (* table for mapping from (top-level-)label to step_vect position *)
-      fun update_table (i, Prove (_, _, l, _, _)) = Label_Table.update_new (l, i)
+      fun update_table (i, Prove (_, _, l, _, _, _)) =
+            Label_Table.update_new (l, i)
         | update_table _ = I
       val label_index_table = fold_index update_table steps Label_Table.empty
       val lookup_indices = map_filter (Label_Table.lookup label_index_table)
 
       (* proof step references *)
       fun refs step =
-        (case byline_of_step step of
-          NONE => []
-        | SOME (By_Metis (subproofs, (lfs, _))) =>
-            maps (steps_of_proof #> maps refs) subproofs @ lookup_indices lfs)
+        fold_isar_step
+          (byline_of_step
+           #> (fn SOME (By_Metis (lfs, _)) => append (lookup_indices lfs)
+                | _ => I))
+          step []
       val refed_by_vect =
         Vector.tabulate (Vector.length step_vect, K [])
         |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) steps
         |> Vector.map rev (* after rev, indices are sorted in ascending order *)
 
       (* candidates for elimination, use table as priority queue (greedy
          algorithm) *)
       fun add_if_cand step_vect (i, [j]) =
           ((case (the (get i step_vect), the (get j step_vect)) of
-            (Prove (_, Fix [], _, t, By_Metis _), Prove (_, _, _, _, By_Metis _)) =>
-              cons (Term.size_of_term t, i)
+            (Prove (_, Fix [], _, t, _, By_Metis _),
+             Prove (_, _, _, _, _, By_Metis _)) => cons (Term.size_of_term t, i)
           | _ => I)
             handle Option.Option => raise Fail "sledgehammer_compress: add_if_cand")
         | add_if_cand _ _ = I
       val cand_tab =
         v_fold_index (add_if_cand step_vect) refed_by_vect []

           (apfst get_time #> uncurry add_preplay_time)
           zero_preplay_time lazy_time_vector
 
       (* Merging *)
       fun merge
-          (Prove (_, Fix [], lbl1, _, By_Metis (subproofs1, (lfs1, gfs1))))
-          (Prove (qs2, fix, lbl2, t, By_Metis (subproofs2, (lfs2, gfs2)))) =
+          (Prove (_, Fix [], lbl1, _, subproofs1, By_Metis (lfs1, gfs1)))
+          (Prove (qs2, fix, lbl2, t, subproofs2, By_Metis (lfs2, gfs2))) =
             let
               val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1
               val gfs = union (op =) gfs1 gfs2
               val subproofs = subproofs1 @ subproofs2
-            in Prove (qs2, fix, lbl2, t, By_Metis (subproofs, (lfs, gfs))) end
+            in Prove (qs2, fix, lbl2, t, subproofs, By_Metis (lfs, gfs)) end
         | merge _ _ = raise Fail "sledgehammer_compress: unmergeable Isar steps"
 
       fun try_merge metis_time (s1, i) (s2, j) =
         if not preplay then (merge s1 s2 |> SOME, metis_time)
         else

         val thy = Proof_Context.theory_of ctxt
         (* TODO: add Skolem variables to context? *)
         fun enrich_with_fact l t =
           Proof_Context.put_thms false
               (string_of_label l, SOME [Skip_Proof.make_thm thy t])
-        fun enrich_with_step (Prove (_, _, l, t, _)) = enrich_with_fact l t
+        fun enrich_with_step (Prove (_, _, l, t, _, _)) = enrich_with_fact l t
           | enrich_with_step _ = I
         val enrich_with_steps = fold enrich_with_step
         val enrich_with_assms = fold (uncurry enrich_with_fact)
         val rich_ctxt =
           ctxt |> enrich_with_assms assms |> enrich_with_steps steps

         fun compress_each_and_collect_time compress subproofs =
           let fun f_m proof time = compress proof ||> add_preplay_time time
           in fold_map f_m subproofs zero_preplay_time end
         val compress_subproofs =
           compress_each_and_collect_time (do_proof false ctxt)
-        fun compress (Prove (qs, fix, l, t, By_Metis(subproofs, facts))) =
+        fun compress (Prove (qs, fix, l, t, subproofs, By_Metis facts)) =
               let val (subproofs, time) = compress_subproofs subproofs
-              in (Prove (qs, fix, l, t, By_Metis(subproofs, facts)), time) end
+              in (Prove (qs, fix, l, t, subproofs, By_Metis  facts), time) end
           | compress atomic_step = (atomic_step, zero_preplay_time)
       in
         compress_each_and_collect_time compress subproofs
       end
   in