# HG changeset patch
# User blanchet
# Date 1380898835 -7200
# Node ID 183cfce3f82740b8b440c8bc886ef846bc7cc2df
# Parent  c0658286aa08fdf3c59a86e3cf4ed379bee61f55
more tracing

diff -r c0658286aa08 -r 183cfce3f827 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Oct 04 16:51:26 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Oct 04 17:00:35 2013 +0200
@@ -974,7 +974,7 @@
     val (access_G, suggs) =
       peek_state ctxt overlord (fn {access_G, ...} =>
           if Graph.is_empty access_G then
-            (access_G, [])
+            (trace_msg ctxt (K "Nothing has been learned yet"); (access_G, []))
           else
             let
               val parents = maximal_wrt_access_graph access_G facts