equal
deleted
inserted
replaced
475 hyp_ts concl_t |
475 hyp_ts concl_t |
476 |> filter (is_appropriate_prop o prop_of o snd) |
476 |> filter (is_appropriate_prop o prop_of o snd) |
477 |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name |
477 |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name |
478 (the_default default_max_facts max_facts) |
478 (the_default default_max_facts max_facts) |
479 Sledgehammer_Fact.no_fact_override hyp_ts concl_t |
479 Sledgehammer_Fact.no_fact_override hyp_ts concl_t |
|
480 |> #1 (*###*) |
480 |> map (apfst (apfst (fn name => name ()))) |
481 |> map (apfst (apfst (fn name => name ()))) |
481 |> tap (fn facts => |
482 |> tap (fn facts => |
482 "Line " ^ str0 (Position.line_of pos) ^ ": " ^ |
483 "Line " ^ str0 (Position.line_of pos) ^ ": " ^ |
483 (if null facts then |
484 (if null facts then |
484 "Found no relevant facts." |
485 "Found no relevant facts." |