src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML

               | (SOME (l, _), candidates') =>
                 (case find_index (curry (op =) (SOME l) o label_of_isar_step) steps of
                   ~1 => steps
                 | i =>
                   let val successors = get_successors l in
-                    if length successors > compress_degree then steps
-                    else compression_loop candidates' (try_eliminate i l successors steps)
+                    if length successors > compress_degree then
+                      steps
+                    else
+                      steps
+                      |> not (null successors) ? try_eliminate i l successors
+                      |> compression_loop candidates'
                   end))
 
           fun add_cand (Prove (_, _, l, t, _, _, _, _)) = cons (l, size_of_term t)
             | add_cand _ = I