src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

             |> Output.urgent_message
           else
             ()
         val birth = Timer.checkRealTimer timer
         val _ =
-          if debug then
-            Output.urgent_message "Invoking SMT solver..."
-          else
-            ()
+          if debug then Output.urgent_message "Invoking SMT solver..." else ()
         val (outcome, used_facts) =
           SMT_Solver.smt_filter remote iter_timeout state facts i
           |> (fn {outcome, used_facts, ...} => (outcome, used_facts))
           handle exn => if Exn.is_interrupt exn then
                           reraise exn

                |> warning
              else
                ();
              true (* kind of *))
           | SOME SMT_Failure.Out_Of_Memory => true
-          | SOME _ => true
+          | SOME (SMT_Failure.Other_Failure _) => true
         val timeout = Time.- (timeout, Timer.checkRealTimer timer)
       in
         if too_many_facts_perhaps andalso iter_num < !smt_max_iter andalso
            num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then
           let