equal
deleted
inserted
replaced
437 |
437 |
438 fun relevance_filter ctxt thres0 decay max_facts |
438 fun relevance_filter ctxt thres0 decay max_facts |
439 (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts concl_t = |
439 (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts concl_t = |
440 let |
440 let |
441 val thy = Proof_Context.theory_of ctxt |
441 val thy = Proof_Context.theory_of ctxt |
442 val facts = drop_duplicate_facts facts |
|
443 val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty |
442 val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty |
444 val add_pconsts = add_pconsts_in_term thy |
443 val add_pconsts = add_pconsts_in_term thy |
445 val chained_ts = |
444 val chained_ts = |
446 facts |> map_filter (fn ((_, (Chained, _)), th) => SOME (prop_of th) |
445 facts |> map_filter (fn ((_, (Chained, _)), th) => SOME (prop_of th) |
447 | _ => NONE) |
446 | _ => NONE) |