src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

                       extract_tstplike_proof_and_outcome verbose proof_delims known_failures output
                       |>> atp_proof_of_tstplike_proof atp_problem
                       handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)))
               handle TimeLimit.TimeOut => (("", slice_timeout), ([], SOME TimedOut))
             val outcome =
-              case outcome of
+              (case outcome of
                 NONE =>
                 (case used_facts_in_unsound_atp_proof ctxt fact_names atp_proof
                       |> Option.map (sort string_ord) of
                    SOME facts =>
-                   let
-                     val failure =
-                       UnsoundProof (is_type_enc_sound type_enc, facts)
-                   in
-                     if debug then
-                       (warning (string_of_atp_failure failure); NONE)
-                     else
-                       SOME failure
+                   let val failure = UnsoundProof (is_type_enc_sound type_enc, facts) in
+                     if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure
                    end
                  | NONE => NONE)
-              | _ => outcome
+              | _ => outcome)
           in
             ((SOME key, value), (output, run_time, facts, atp_proof, outcome))
           end
         val timer = Timer.startRealTimer ()
         fun maybe_run_slice slice

             in
               if Time.<= (time_left, Time.zeroTime) then
                 result
               else
                 run_slice time_left cache slice
-                |> (fn (cache, (output, run_time, used_from, atp_proof,
-                                outcome)) =>
-                       (cache, (output, Time.+ (run_time0, run_time), used_from,
-                                atp_proof, outcome)))
+                |> (fn (cache, (output, run_time, used_from, atp_proof, outcome)) =>
+                  (cache, (output, Time.+ (run_time0, run_time), used_from, atp_proof, outcome)))
             end
           | maybe_run_slice _ result = result
       in
         ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)),
          ("", Time.zeroTime, [], [], SOME InternalError))

         NONE =>
         let
           val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
           val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
           val reconstrs =
-            bunch_of_reconstructors needs_full_types
-                (lam_trans_of_atp_proof atp_proof
-                 o (fn desperate => if desperate then hide_lamsN
-                                    else default_metis_lam_trans))
+            bunch_of_reconstructors needs_full_types (lam_trans_of_atp_proof atp_proof
+              o (fn desperate => if desperate then hide_lamsN else default_metis_lam_trans))
         in
           (used_facts,
            Lazy.lazy (fn () =>
              let
                val used_pairs =