author | blanchet |
Sun, 13 Jan 2013 22:00:45 +0100 | |
changeset 50868 | 4b30d461b3a6 |
parent 50867 | 48836c35d636 |
child 50869 | 67bb94a6f780 |
child 50872 | a9f07af30d64 |
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun Jan 13 21:42:39 2013 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun Jan 13 22:00:45 2013 +0100 @@ -479,6 +479,7 @@ Sledgehammer_Fact.no_fact_override hyp_ts concl_t |> map (apfst (apfst (fn name => name ()))) |> tap (fn facts => + "Line " ^ str0 (Position.line_of pos) ^ ": " ^ (if null facts then "Found no relevant facts." else