# HG changeset patch
# User blanchet
# Date 1377260397 -7200
# Node ID 496db18077fabddc17d8446526113af660dbd5e0
# Parent  1e9735cd27aa213c226306ccfbcef998347eacc9
tuned output

diff -r 1e9735cd27aa -r 496db18077fa src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Aug 23 14:04:08 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Aug 23 14:19:57 2013 +0200
@@ -1314,7 +1314,7 @@
                andalso length (filter_out is_in_access_G facts)
                        <= max_facts_to_learn_before_query then
               (mash_learn_facts ctxt params prover false 2 false timeout facts
-               |> (fn "" => () | s => Output.urgent_message s);
+               |> (fn "" => () | s => Output.urgent_message (MaShN ^ ": " ^ s);
                true)
             else
               (maybe_launch_thread (); false)