src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

           | (_, outcome) => string_of_play_outcome outcome)
 
         val (play_outcome, isar_proof) =
           canonical_isar_proof
           |> tap (trace_isar_proof "Original")
-          |> compress_isar_proof ctxt compress_isar preplay_data
+          |> compress_isar_proof ctxt compress_isar preplay_timeout preplay_data
           |> tap (trace_isar_proof "Compressed")
           |> postprocess_isar_proof_remove_unreferenced_steps
                (keep_fastest_method_of_isar_step (!preplay_data)
                 #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
           |> tap (trace_isar_proof "Minimized")
+          (* It's not clear whether this is worth the trouble (and if so, "isar_compress" has an
+             unnatural semantics): *)
+(*
           |> minimize
-               ? (compress_isar_proof ctxt compress_isar preplay_data
+               ? (compress_isar_proof ctxt compress_isar preplay_timeout preplay_data
                   #> tap (trace_isar_proof "Compressed again"))
+*)
           |> `(preplay_outcome_of_isar_proof (!preplay_data))
           ||> (comment_isar_proof comment_of
                #> chain_isar_proof
                #> kill_useless_labels_in_isar_proof
                #> relabel_isar_proof_nicely)