changeset 51004 | 5f2788c38127 |
parent 51003 | 198cb05fb35b |
child 51005 | ce4290c33d73 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Jan 31 17:54:05 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Jan 31 17:54:05 2013 +0100 @@ -237,7 +237,6 @@ |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t |> #1 (*###*) - |> map (apfst (apfst (fn name => name ()))) |> tap (fn facts => if verbose then label ^ plural_s (length provers) ^ ": " ^