src/HOL/Tools/Sledgehammer/sledgehammer_run.ML

   else case subgoal_count state of
     0 => (Output.urgent_message "No subgoal!"; (false, state))
   | n =>
     let
       val _ = Proof.assert_backward state
+      val print = if auto then K () else Output.urgent_message
       val state =
         state |> Proof.map_context (Config.put SMT_Config.verbose debug)
       val ctxt = Proof.context_of state
       val thy = ProofContext.theory_of ctxt
       val {facts = chained_ths, goal, ...} = Proof.goal state

       val no_dangerous_types = types_dangerous_types type_sys
       val _ = () |> not blocking ? kill_provers
       val _ = case find_first (not o is_prover_supported ctxt) provers of
                 SOME name => error ("No such prover: " ^ name ^ ".")
               | NONE => ()
-      val _ = if auto then () else Output.urgent_message "Sledgehammering..."
+      val _ = print "Sledgehammering..."
       val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)
       fun launch_provers state get_facts translate maybe_smt_filter provers =
         let
           val facts = get_facts ()
           val num_facts = length facts

                           "Found no relevant facts."
                         else
                           "Including (up to) " ^ string_of_int (length facts) ^
                           " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
                           (facts |> map (fst o fst) |> space_implode " ") ^ ".")
-                       |> Output.urgent_message
+                       |> print
                      else
                        ())
         end
       fun launch_atps accum =
         if null atps then

                  |> exists fst |> rpair state
           end
       fun launch_atps_and_smt_solvers () =
         [launch_atps, launch_smts]
         |> smart_par_list_map (fn f => f (false, state) |> K ())
-        handle ERROR msg => (Output.urgent_message ("Error: " ^ msg); error msg)
+        handle ERROR msg => (print ("Error: " ^ msg); error msg)
     in
       (false, state)
       |> (if blocking then launch_atps #> not auto ? launch_smts
           else (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))
+      handle TimeLimit.TimeOut =>
+             (print "Sledgehammer ran out of time."; (false, state))
     end
 
 end;