changeset 50868 | 4b30d461b3a6 |
parent 50867 | 48836c35d636 |
child 51003 | 198cb05fb35b |
--- 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