changeset 51003 | 198cb05fb35b |
parent 50868 | 4b30d461b3a6 |
child 51004 | 5f2788c38127 |
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jan 31 17:42:12 2013 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jan 31 17:54:05 2013 +0100 @@ -477,6 +477,7 @@ |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name (the_default default_max_facts max_facts) Sledgehammer_Fact.no_fact_override hyp_ts concl_t + |> #1 (*###*) |> map (apfst (apfst (fn name => name ()))) |> tap (fn facts => "Line " ^ str0 (Position.line_of pos) ^ ": " ^