src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML

 
 open Sledgehammer_Reconstructor
 open Sledgehammer_Isar_Proof
 open Sledgehammer_Isar_Preplay
 
-fun keep_fastest_method_of_isar_step preplay_data
-      (Prove (qs, xs, l, t, subproofs, (facts, _))) =
-    Prove (qs, xs, l, t, subproofs, (facts, [fastest_method_of_isar_step preplay_data l]))
+fun keep_fastest_method_of_isar_step preplay_data (Prove (qs, xs, l, t, subproofs, facts, _)) =
+    Prove (qs, xs, l, t, subproofs, facts, [fastest_method_of_isar_step preplay_data l])
   | keep_fastest_method_of_isar_step _ step = step
 
 val slack = seconds 0.1
 
 fun minimize_isar_step_dependencies ctxt preplay_data
-      (step as Prove (qs, xs, l, t, subproofs, ((lfs0, gfs0), meths as meth :: _))) =
+      (step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _)) =
     (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
       Played time =>
       let
-        fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))
+        fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths)
 
         fun minimize_facts _ time min_facts [] = (time, min_facts)
           | minimize_facts mk_step time min_facts (f :: facts) =
             (case preplay_isar_step_for_method ctxt (Time.+ (time, slack)) meth
                 (mk_step (min_facts @ facts)) of

         if Ord_List.member label_ord used l then
           process_used_step step |>> Ord_List.union label_ord used ||> (fn step => step :: accu)
         else
           (used, accu))
     and process_used_step step = step |> postproc_step |> process_used_step_subproofs
-    and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))) =
+    and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths)) =
       let
         val (used, subproofs) =
           map process_proof subproofs
           |> split_list
           |>> Ord_List.unions label_ord
           |>> fold (Ord_List.insert label_ord) lfs
-        val step = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))
       in
-        (used, step)
+        (used, Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths))
       end
   in
     snd o process_proof
   end