--- 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)