# HG changeset patch
# User blanchet
# Date 1379940823 -7200
# Node ID 58d1b63bea81e4f596635460d1ba9c51aa49807f
# Parent  b6a947a2c615a0b8ba2fe486e651faadb83e3f4e
tuned spying

diff -r b6a947a2c615 -r 58d1b63bea81 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon Sep 23 14:53:43 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon Sep 23 14:53:43 2013 +0200
@@ -225,7 +225,7 @@
                 SOME name => error ("No such prover: " ^ name ^ ".")
               | NONE => ()
       val _ = print "Sledgehammering..."
-      val _ = spying spy (fn () => ("***", "run"))
+      val _ = spying spy (fn () => ("***", "starting " ^ @{make_string} mode ^ " mode"))
       val (smts, (ueq_atps, full_atps)) =
         provers |> List.partition (is_smt_prover ctxt)
                 ||> List.partition (is_unit_equational_atp ctxt)