author | wenzelm |
Sun, 13 Jan 2013 22:09:24 +0100 | |
changeset 50872 | a9f07af30d64 |
parent 50871 | 2ea3c90ff0bb (current diff) |
parent 50868 | 4b30d461b3a6 (diff) |
child 50873 | 3afe082ff9cd |
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun Jan 13 22:07:00 2013 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun Jan 13 22:09:24 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