src/HOL/Tools/Sledgehammer/sledgehammer_print.ML

 fun one_line_proof_text num_chained
     (preplay, banner, used_facts, minimize_command, subgoal, subgoal_count) =
   let
     val (chained, extra) = split_used_facts used_facts
     val (failed, reconstr, ext_time) =
-      case preplay of
+      (case preplay of
         Played (reconstr, time) => (false, reconstr, (SOME (false, time)))
       | Play_Timed_Out (reconstr, time) =>
-        (false, reconstr,
-         (case time of
-           NONE => NONE
-         | SOME time => if time = Time.zeroTime then NONE else SOME (true, time)))
-      | Play_Failed reconstr => (true, reconstr, NONE)
+        (false, reconstr, if time = Time.zeroTime then NONE else SOME (true, time))
+      | Play_Failed reconstr => (true, reconstr, NONE))
     val try_line =
       ([], map fst extra)
       |> reconstructor_command reconstr subgoal subgoal_count (map fst chained) num_chained
       |> (if failed then
             enclose "One-line proof reconstruction failed: "