src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML

     and update_subproofs [] updates = ([], updates)
       | update_subproofs steps [] = (steps, [])
       | update_subproofs (proof :: subproofs) updates =
         update_proof proof (update_subproofs subproofs updates)
     and update_proof proof (proofs, []) = (proof :: proofs, [])
-      | update_proof (Proof (xs, assms, steps)) (proofs, updates) =
+      | update_proof (Proof {fixes, assumptions, steps}) (proofs, updates) =
         let val (steps', updates') = update_steps steps updates in
-          (Proof (xs, assms, steps') :: proofs, updates')
+          (Proof {fixes = fixes, assumptions = assumptions, steps = steps'} :: proofs, updates')
         end
   in
     fst (update_steps steps (rev updates))
   end
 

           nontriv_subs =
         if null subs orelse not (compress_further ()) then
           Prove (qs, xs, l, t, List.revAppend (nontriv_subs, subs), (lfs, gfs), meths, comment)
         else
           (case subs of
-            (sub as Proof (_, assms, [Prove (_, _, l', _, [], (lfs', gfs'), meths', _)])) :: subs =>
+            (sub as Proof {assumptions,
+              steps = [Prove (_, _, l', _, [], (lfs', gfs'), meths', _)], ...}) :: subs =>
             let
               (* merge steps *)
               val subs'' = subs @ nontriv_subs
-              val lfs'' = union (op =) lfs (subtract (op =) (map fst assms) lfs')
+              val lfs'' = union (op =) lfs (subtract (op =) (map fst assumptions) lfs')
               val gfs'' = union (op =) gfs' gfs
               val (meths'' as _ :: _, hopeless) =
                 merge_methods (!preplay_data) (l', meths') (l, meths)
               val step'' = Prove (qs, xs, l, t, subs'', (lfs'', gfs''), meths'', comment)
 

          proof level, the proof steps have no subproofs. In the best case, these steps can be merged
          into just one step, resulting in a trivial subproof. Going one level up, trivial subproofs
          can be eliminated. In the best case, this once again leads to a proof whose proof steps do
          not have subproofs. Applying this approach recursively will result in a flat proof in the
          best cast. *)
-      fun compress_proof (proof as (Proof (xs, assms, steps))) =
-        if compress_further () then Proof (xs, assms, compress_steps steps) else proof
+      fun compress_proof (proof as (Proof {fixes, assumptions, steps})) =
+        if compress_further () then
+          Proof {fixes = fixes, assumptions = assumptions, steps = compress_steps steps}
+        else
+          proof
       and compress_steps steps =
         (* bottom-up: compress innermost proofs first *)
         steps
         |> map (fn step => step |> compress_further () ? compress_sub_levels)
         |> compress_further () ? compress_top_level