drop chained facts
authorblanchet
Fri Aug 27 15:37:03 2010 +0200 (2010-08-27)
changeset 38826f42f425edf24
parent 38825 4ec3cbd95f25
child 38827 cf01645cbbce
drop chained facts
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Aug 27 13:27:02 2010 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Aug 27 15:37:03 2010 +0200
     1.3 @@ -357,15 +357,16 @@
     1.4      case result of
     1.5        SH_OK (time_isa, time_atp, names) =>
     1.6          let
     1.7 -          fun get_thms (name, loc) =
     1.8 -            ((name, loc), thms_of_name (Proof.context_of st) name)
     1.9 +          fun get_thms (name, Sledgehammer_Fact_Filter.Chained) = NONE
    1.10 +            | get_thms (name, loc) =
    1.11 +              SOME ((name, loc), thms_of_name (Proof.context_of st) name)
    1.12          in
    1.13            change_data id inc_sh_success;
    1.14            change_data id (inc_sh_lemmas (length names));
    1.15            change_data id (inc_sh_max_lems (length names));
    1.16            change_data id (inc_sh_time_isa time_isa);
    1.17            change_data id (inc_sh_time_atp time_atp);
    1.18 -          named_thms := SOME (map get_thms names);
    1.19 +          named_thms := SOME (map_filter get_thms names);
    1.20            log (sh_tag id ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
    1.21              string_of_int time_atp ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
    1.22          end