# 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