src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
changeset 49358 0fa351b1bd14
parent 48798 9152e66f98da
child 49914 23e36a4d28f1
equal deleted inserted replaced
49357:34ac36642a31 49358:0fa351b1bd14
   135         (outcome_code,
   135         (outcome_code,
   136          state
   136          state
   137          |> outcome_code = someN
   137          |> outcome_code = someN
   138             ? Proof.goal_message (fn () =>
   138             ? Proof.goal_message (fn () =>
   139                   [Pretty.str "",
   139                   [Pretty.str "",
   140                    Pretty.mark Isabelle_Markup.hilite (Pretty.str (message ()))]
   140                    Pretty.mark Isabelle_Markup.intensify (Pretty.str (message ()))]
   141                   |> Pretty.chunks))
   141                   |> Pretty.chunks))
   142       end
   142       end
   143     else if blocking then
   143     else if blocking then
   144       let
   144       let
   145         val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()
   145         val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()