changeset 48289 | 6b65f1ad0e4b |
parent 48288 | 255c6e1fd505 |
child 48292 | 7fcee834c7f5 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jul 18 08:44:03 2012 +0200 @@ -225,6 +225,7 @@ | NONE => I) |> relevant_facts ctxt params (hd provers) max_max_relevant relevance_override chained_ths hyp_ts concl_t + |> map (apfst (apfst (fn name => name ()))) |> tap (fn facts => if debug then label ^ plural_s (length provers) ^ ": " ^