src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 50442 4f6a4d32522c
parent 50239 fb579401dc26
child 50481 5d147d492792
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Dec 08 13:55:26 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Dec 08 21:54:28 2012 +0100
     1.3 @@ -30,7 +30,7 @@
     1.4      -> (((unit -> string) * 'a) * thm) list
     1.5    val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
     1.6    val all_facts :
     1.7 -    Proof.context -> bool -> unit Symtab.table -> thm list -> thm list
     1.8 +    Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list
     1.9      -> status Termtab.table -> fact list
    1.10    val nearly_all_facts :
    1.11      Proof.context -> bool -> fact_override -> unit Symtab.table
    1.12 @@ -145,7 +145,7 @@
    1.13  (* FIXME: put other record thms here, or declare as "no_atp" *)
    1.14  fun multi_base_blacklist ctxt ho_atp =
    1.15    ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
    1.16 -   "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
    1.17 +   "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
    1.18     "weak_case_cong", "nibble_pair_of_char_simps", "nibble.simps",
    1.19     "nibble.distinct"]
    1.20    |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
    1.21 @@ -370,7 +370,7 @@
    1.22  fun maybe_filter_no_atps ctxt =
    1.23    not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
    1.24  
    1.25 -fun all_facts ctxt ho_atp reserved add_ths chained css =
    1.26 +fun all_facts ctxt really_all ho_atp reserved add_ths chained css =
    1.27    let
    1.28      val thy = Proof_Context.theory_of ctxt
    1.29      val global_facts = Global_Theory.facts_of thy
    1.30 @@ -387,14 +387,15 @@
    1.31        Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
    1.32      fun add_facts global foldx facts =
    1.33        foldx (fn (name0, ths) =>
    1.34 -        if name0 <> "" andalso
    1.35 +        if not really_all andalso
    1.36 +           name0 <> "" andalso
    1.37             forall (not o member Thm.eq_thm_prop add_ths) ths andalso
    1.38             (Facts.is_concealed facts name0 orelse
    1.39              not (can (Proof_Context.get_thms ctxt) name0) orelse
    1.40              (not (Config.get ctxt ignore_no_atp) andalso
    1.41               is_package_def name0) orelse
    1.42              exists (fn s => String.isSuffix s name0)
    1.43 -                   (multi_base_blacklist ctxt ho_atp)) then
    1.44 +                    (multi_base_blacklist ctxt ho_atp)) then
    1.45            I
    1.46          else
    1.47            let
    1.48 @@ -453,7 +454,7 @@
    1.49                 o fact_from_ref ctxt reserved chained css) add
    1.50         else
    1.51           let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
    1.52 -           all_facts ctxt ho_atp reserved add chained css
    1.53 +           all_facts ctxt false ho_atp reserved add chained css
    1.54             |> filter_out (member Thm.eq_thm_prop del o snd)
    1.55             |> maybe_filter_no_atps ctxt
    1.56             |> uniquify