# HG changeset patch # User blanchet # Date 1355000068 -3600 # Node ID 4f6a4d32522c76a9cae33c3e4d6cc28966af988b # Parent 1e71f9d3cd57d2dbebb75e8ea54f8e147e7f5c24 don't blacklist "case" theorems -- this causes problems in MaSh later diff -r 1e71f9d3cd57 -r 4f6a4d32522c src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Sat Dec 08 13:55:26 2012 +0100 +++ b/src/HOL/TPTP/atp_theory_export.ML Sat Dec 08 21:54:28 2012 +0100 @@ -123,7 +123,7 @@ val path = file_name |> Path.explode val _ = File.write path "" val facts = - Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) false + Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true false Symtab.empty [] [] css_table val atp_problem = facts diff -r 1e71f9d3cd57 -r 4f6a4d32522c src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Sat Dec 08 13:55:26 2012 +0100 +++ b/src/HOL/TPTP/mash_eval.ML Sat Dec 08 21:54:28 2012 +0100 @@ -38,7 +38,7 @@ val sugg_path = sugg_file_name |> Path.explode val lines = sugg_path |> File.read_lines val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt - val facts = all_facts ctxt false Symtab.empty [] [] css + val facts = all_facts ctxt true false Symtab.empty [] [] css val all_names = all_names (facts |> map snd) val mepo_ok = Unsynchronized.ref 0 val mash_ok = Unsynchronized.ref 0 diff -r 1e71f9d3cd57 -r 4f6a4d32522c src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Sat Dec 08 13:55:26 2012 +0100 +++ b/src/HOL/TPTP/mash_export.ML Sat Dec 08 21:54:28 2012 +0100 @@ -44,7 +44,7 @@ fun all_facts ctxt = let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in - Sledgehammer_Fact.all_facts ctxt false Symtab.empty [] [] css + Sledgehammer_Fact.all_facts ctxt true false Symtab.empty [] [] css end fun add_thy_parent_facts thy_map thy = diff -r 1e71f9d3cd57 -r 4f6a4d32522c src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sat Dec 08 13:55:26 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sat Dec 08 21:54:28 2012 +0100 @@ -30,7 +30,7 @@ -> (((unit -> string) * 'a) * thm) list val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list val all_facts : - Proof.context -> bool -> unit Symtab.table -> thm list -> thm list + Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list -> status Termtab.table -> fact list val nearly_all_facts : Proof.context -> bool -> fact_override -> unit Symtab.table @@ -145,7 +145,7 @@ (* FIXME: put other record thms here, or declare as "no_atp" *) fun multi_base_blacklist ctxt ho_atp = ["defs", "select_defs", "update_defs", "split", "splits", "split_asm", - "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong", + "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong", "weak_case_cong", "nibble_pair_of_char_simps", "nibble.simps", "nibble.distinct"] |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ? @@ -370,7 +370,7 @@ fun maybe_filter_no_atps ctxt = not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd) -fun all_facts ctxt ho_atp reserved add_ths chained css = +fun all_facts ctxt really_all ho_atp reserved add_ths chained css = let val thy = Proof_Context.theory_of ctxt val global_facts = Global_Theory.facts_of thy @@ -387,14 +387,15 @@ Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts) fun add_facts global foldx facts = foldx (fn (name0, ths) => - if name0 <> "" andalso + if not really_all andalso + name0 <> "" andalso forall (not o member Thm.eq_thm_prop add_ths) ths andalso (Facts.is_concealed facts name0 orelse not (can (Proof_Context.get_thms ctxt) name0) orelse (not (Config.get ctxt ignore_no_atp) andalso is_package_def name0) orelse exists (fn s => String.isSuffix s name0) - (multi_base_blacklist ctxt ho_atp)) then + (multi_base_blacklist ctxt ho_atp)) then I else let @@ -453,7 +454,7 @@ o fact_from_ref ctxt reserved chained css) add else let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in - all_facts ctxt ho_atp reserved add chained css + all_facts ctxt false ho_atp reserved add chained css |> filter_out (member Thm.eq_thm_prop del o snd) |> maybe_filter_no_atps ctxt |> uniquify