author | blanchet |
Fri, 04 Oct 2013 17:00:35 +0200 | |
changeset 54064 | 183cfce3f827 |
parent 54063 | c0658286aa08 |
child 54065 | e30e63d05e58 |
--- 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